PDF de programación - Lógica computacional

Lógica computacional

José A. Alonso Jiménez

Febrero de 1997

Depto. de Ciencias de la Computación e Inteligencia Artificial

Universidad de Sevilla

Contenido

1 Preliminares

1.1 Cadenas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.2
Inducción y recursión . . . . . . . . . . . . . . . . . . . . . . .

2 Sintaxis de la lógica proposicional

2.1 El lenguaje de la lógica proposicional
2.2 Libre generación del conjunto de las fórmulas

. . . . . . . . . . . . . .
. . . . . . . . .

3 Semántica de la lógica proposicional

3.1 La semántica de las proposiciones . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . .
3.2 Tautologías
3.3 Métodos de verificación de tautologías
. . . . . . . . . . . . .

1
1
2

4
4
5

7
7
8
9

4 Completitud funcional y compacidad

11
4.1 Completitud funcional
. . . . . . . . . . . . . . . . . . . . . . 11
4.2 Compacidad . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

5 Equivalencia y formas normales

13
5.1 Equivalencia . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
5.2 Formas normales
. . . . . . . . . . . . . . . . . . . . . . . . . 14
5.3 Formas normales y validez . . . . . . . . . . . . . . . . . . . . 16

6 Cláusulas proposicionales

18
6.1 Cláusulas
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
6.2 Cláusulas y fórmulas . . . . . . . . . . . . . . . . . . . . . . . 19

7 El algoritmo de Davis–Putnam

21
7.1 Las reglas de Davis–Putnam . . . . . . . . . . . . . . . . . . . 21
7.2 El algoritmo de Davis–Putnam . . . . . . . . . . . . . . . . . 22
7.3
Inconsistencia minimal y subsunción . . . . . . . . . . . . . . 23

8 Resolución proposicional

24
8.1 Sistema de resolución . . . . . . . . . . . . . . . . . . . . . . . 24
8.2 Correción y completitud de la resolución . . . . . . . . . . . . 25
8.3 Estrategias de resolución . . . . . . . . . . . . . . . . . . . . . 25

ii

CONTENIDO

iii

9 Refinamientos de resolución

27
9.1 Resolución semántica . . . . . . . . . . . . . . . . . . . . . . . 27
9.2 Resolución P1 y N1 . . . . . . . . . . . . . . . . . . . . . . . . 29
9.3 Resolución lineal
. . . . . . . . . . . . . . . . . . . . . . . . . 32
9.4 Resolución con soporte . . . . . . . . . . . . . . . . . . . . . . 33
9.5 Resolución unidad y por entradas . . . . . . . . . . . . . . . . 34

10 Cláusulas de Horn

37
10.1 Cláusulas de Horn . . . . . . . . . . . . . . . . . . . . . . . . 37
10.2 Resolución y cláusulas de Horn . . . . . . . . . . . . . . . . . 37
10.3 Resolución SLD . . . . . . . . . . . . . . . . . . . . . . . . . . 38

11 Sintaxis de la lógica de primer orden

40
11.1 El lenguaje de la lógica de primer orden . . . . . . . . . . . . 40
11.2 Libre generación de términos y fórmulas
. . . . . . . . . . . . 43
11.3 Variables libres y ligadas . . . . . . . . . . . . . . . . . . . . . 44
11.4 Sustituciones
. . . . . . . . . . . . . . . . . . . . . . . . . . . 44

12 Semántica de la lógica de primer orden

47
12.1 Semántica de los términos y las fórmulas . . . . . . . . . . . . 47
12.2 Consistencia, validez y modelos
. . . . . . . . . . . . . . . . . 48
12.3 Semántica mediante extensiones de lenguajes . . . . . . . . . . 50
12.4 Fórmulas válidas
. . . . . . . . . . . . . . . . . . . . . . . . . 50

13 Formas normales y cláusulas

53
13.1 Formas prenexas
. . . . . . . . . . . . . . . . . . . . . . . . . 53
13.2 Formas de Skolem . . . . . . . . . . . . . . . . . . . . . . . . . 53
. . . . . . . . . . . . . . . . . . . . . . . . . 54
13.3 Formas clausales

14 Cláusulas de primer orden

55
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
14.1 Cláusulas
14.2 Cláusulas y fórmulas . . . . . . . . . . . . . . . . . . . . . . . 57

15 Teorema de Herbrand

59
15.1 Modelos de Herbrand . . . . . . . . . . . . . . . . . . . . . . . 59
15.2 Teorema de Herbrand . . . . . . . . . . . . . . . . . . . . . . . 61
15.3 Métodos de deducción basados directamente en el teorema de

Herbrand . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
15.4 Resolución básica . . . . . . . . . . . . . . . . . . . . . . . . . 62

16 Sustitución y unificación

64
16.1 Comparación de términos
. . . . . . . . . . . . . . . . . . . . 64
16.2 Comparación de sustituciones . . . . . . . . . . . . . . . . . . 66
16.3 Unificación . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
16.4 Unificación para fórmulas atómicas
. . . . . . . . . . . . . . . 69

José A. Alonso

Lógica computacional

(Sevilla, Febrero, 1997)

CONTENIDO

iv

17 Resolución en lógica de primer orden

72
17.1 Sistema de resolución . . . . . . . . . . . . . . . . . . . . . . . 72
17.2 Corrección y completitud de la resolución . . . . . . . . . . . . 74
17.3 Reglas de simplificación . . . . . . . . . . . . . . . . . . . . . 74
17.4 Refinamientos de resolución . . . . . . . . . . . . . . . . . . . 74

18 Programas lógicos: semántica declarativa

75
18.1 Programas lógicos . . . . . . . . . . . . . . . . . . . . . . . . . 75
18.2 Modelos de Herbrand . . . . . . . . . . . . . . . . . . . . . . . 77

19 Programas lógicos: semántica de puntos fijos

78
19.1 Operadores y sus puntos fijos
. . . . . . . . . . . . . . . . . . 78
19.2 El operador de consecuencia inmediata . . . . . . . . . . . . . 80

20 Programas lógicos: semántica procedural

82
20.1 Proceso de computación: La resolución SLD . . . . . . . . . . 82
20.2 Correción de la resolución SLD . . . . . . . . . . . . . . . . . 84
20.3 Completitud de la resolución SLD . . . . . . . . . . . . . . . . 84
20.4 Reglas de computación . . . . . . . . . . . . . . . . . . . . . . 85
20.5 Árboles SLD . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
20.6 Procedimientos de refutación. La evaluación de Prolog . . . . 89

Bibliografía

91

José A. Alonso

Lógica computacional

(Sevilla, Febrero, 1997)

Capítulo 1

Preliminares

1.1 Cadenas

1.1.1 Definición Sea Σ un conjunto no vacío.

1. Una cadena de longitud n en Σ es una aplicación u : n → Σ.
2. La longitud de la cadena u se representa por |u|.

3. El conjunto de las cadenas de longitud n en Σ se representa por Σn.
4. Σ∗ =
5. Las cadenas en Σ son los elementos de Σ∗.

n≥0 Σn.



6. La cadena vacía es el único elemento de Σ0 y se representa por Λ.
7. Si u ∈ Σ∗ y 0 < i ≤ |u|, entonces ui = u(i − 1).
8. Si u ∈ Σn, la cadena u se representa por u1 . . . un.

1.1.2 Definición Dadas dos cadenas u ∈ Σm y v ∈ Σn, su concatenación
(representada por u.v ó uv) es la cadena w ∈ Σm+n definida por



u(i),
v(i − m),

si 0 ≤ i < m;
si m ≤ i < m + n.

w(i) =

1.1.3 Lema

1. Λ es elemento neutro para la concatenación.

2. La concatenación es asociativa.

3. La concatenación no es conmutativa.

1.1.4 Nota Para disminuir el número de paréntesis se usará el convenio de
asociar por la derecha. Por ejemplo, se escribirá uvw en lugar de u.(v.w).

1

Cap. 1. Preliminares

2

1.1.5 Definición Sean u, v ∈ Σ∗.

1. Se dice que u es un prefijo de v (ó v es un sufijo de u), y se representa

por u ≤ v, si existe w ∈ Σ∗ tal que v = uw.

2. Se dice que u es un prefijo propio de v (ó v es un sufijo propio de

u), y se representa por u < v, si u ≤ v y u = v.

1.2 Inducción y recursión

1.2.1 Nota En esta sección usaremos la siguiente notación:

1. A es un conjunto no vacío.
2. F es un conjunto de operaciones en A; es decir, para cada f ∈ F , existe

un n > 0 tal que f : An → A.

3. α es una aplicación de F en N tal que para cada f ∈ F , f : Aα(f ) → A.

Se dice que α(f ) es la aridad de f .

4. X es un subconjunto no vacío de A.

1.2.2 Definición Sea Y ⊆ A.

1. Y es cerrado bajo F si para todo f ∈ F y todo y1, . . . , yα(f ) ∈ Y , se

tiene que f (y1, . . . , yα(f )) ∈ Y .

2. Y es inductivo sobre X si X ⊆ Y e Y es cerrado bajo F .

1.2.3 Definición La clausura transitiva de X es

X + =

{Y ⊆ A : Y es inductivo sobre X}.



1.2.4 Lema X + es el menor subconjunto inductivo de A que contiene a X
y es cerrado bajo F .

1.2.5 Definición

1. La sucesión (Xi)i≥0 está definida recursivamente por:

= X

X0
i }
Xi+1 = Xi ∪ {f (x1, . . . , xn) : f ∈ F, n = α(f ), (x1, . . . , xn) ∈ X n

2. El conjunto engendrado por X mediante F es



i≥0

Xi

X+ =

1.2.6 Lema X + = X+

José A. Alonso

Lógica computacional

(Sevilla, Febrero, 1997)

Cap. 1. Preliminares

3

1.2.7 Teorema (Principio de inducción para X+)
Si Y ⊆ X+ es inductivo sobre X, entonces Y = X+.

1.2.8 Definición Se dice que X+ está libremente generado por X me-
diante F si se verifican las siguientes condiciones:
1. Para toda f ∈ F , la restricción de f a X α(f )
2. Para toda f, g ∈ F , si f = g entonces rang(f ) ∩ rang(g) = ∅.
3. Para toda f ∈ F , rang(f ) ∩ X = ∅.

es inyectiva.

+

1.2.9 Nota En lo que sigue, X−1 = ∅.

1.2.10 Lema Si X+ está libremente generado por X mediante F , entonces
para todo i ≥ 0, se verifican:

1. Si f ∈ F , n = α(f ) y (x1, . . . , xn) ∈ X n

i − X n

f (x1, . . . , xn) /∈ Xi.

i−1, entonces

2. Xi−1 = Xi.

1.2.11 Teorema (de recursión)
Sea B un conjunto no vacío, G un conjunto de operaciones en B, β : G → N
y d : F → G tales que

1. para toda g ∈ G, g es una aplicación de Bβ(g) en B.
2. para toda f ∈ F , β(d(f )) = α(f ).

Si X+ está generado libremente por X mediante F , entonces para cada

aplicación h : X → B existe una única aplicación ˆh : X+ → B tal que:

1. Para todo x ∈ X, ˆh(x) = h(x).
2. Para todo f ∈ F , (x1, . . . , xn) ∈ X n
+,

ˆh(x)(f (x1, . . . , xn)) = g(ˆh(x1), . . . , ˆh(xn)),

donde n = α(f ) y g = d(f ).

José A. Alonso

Lógica computacional

(Sevilla, Febrero, 1997)

Capítulo 2

Sintaxis de la lógica
proposicional

2.1 El lenguaje de la lógica proposicional

2.1.1 Definición El alfabeto proposicional Σ0 consta de:

1. Un conjunto numerable SP de símbolos proposicionales: p0, p1, . . ..
2. Las conectivas lógicas: ¬ (negación) y ∨ (disyunción).

3. Símbolos auxiliares: “(” y “)”.

2.1.2 Definición