PDF de programación - Lógica computacional

Dpto. de Álgebra, Computación, Geometría y Topología

Universidad de Sevilla

Lógica computacional

José A. Alonso Jiménez

([email protected])

Sevilla, 12 de Diciembre de 1991

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

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

4 Completitud funcional y compacidad

4.1 Completitud funcional

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

4.2 Compacidad . . . . . . . . . . . . . . . . . . . . . . . . . . .

5 Equivalencia y formas normales

5.1 Equivalencia . . . . . . . . . . . . . . . . . . . . . . . . . . .

5.2 Formas normales

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

5.3 Formas normales y validez . . . . . . . . . . . . . . . . . . .

6 Cláusulas

6.1 Cláusulas

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

6.2 Cláusulas y fórmulas . . . . . . . . . . . . . . . . . . . . . .

6

6

7

10

10

12

14

14

16

17

19

19

20

21

21

23

24

26

26

28

2

7 El algoritmo de Davis–Putnam

7.1 Las reglas de Davis–Putnam . . . . . . . . . . . . . . . . . .

7.2 El algoritmo de Davis–Putnam . . . . . . . . . . . . . . . .

7.3

Inconsistencia minimal y subsunción . . . . . . . . . . . . .

8 Resolución proposicional

8.1 Sistema de resolución . . . . . . . . . . . . . . . . . . . . . .

8.2 Correción y completitud de la resolución . . . . . . . . . . .

8.3 Estrategias de resolución . . . . . . . . . . . . . . . . . . . .

9 Refinamientos de resolución

9.1 Resolución semántica . . . . . . . . . . . . . . . . . . . . . .

9.2 Resolución P1 y N1 . . . . . . . . . . . . . . . . . . . . . . .

9.3 Resolución lineal

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

9.4 Resolución con soporte . . . . . . . . . . . . . . . . . . . . .

9.5 Resolución unidad y por entradas . . . . . . . . . . . . . . .

10 Cláusulas de Horn

10.1 Cláusulas de Horn . . . . . . . . . . . . . . . . . . . . . . .

10.2 Resolución y cláusulas de Horn . . . . . . . . . . . . . . . .

10.3 Resolución SLD . . . . . . . . . . . . . . . . . . . . . . . . .

11 Sintaxis de la lógica de primer orden

11.1 El lenguaje de la lógica de primer orden . . . . . . . . . . .

11.2 Libre generación de términos y fórmulas

. . . . . . . . . . .

11.3 Variables libres y ligadas . . . . . . . . . . . . . . . . . . . .

11.4 Sustituciones

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

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

12.1 Semántica de los términos y las fórmulas . . . . . . . . . . .

12.2 Consistencia, validez y modelos

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

12.3 Semántica mediante extensiones de lenguajes . . . . . . . . .

12.4 Fórmulas válidas

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

30

30

31

32

33

33

34

35

37

37

39

41

42

44

47

47

48

49

51

51

54

55

56

59

59

60

62

62

3

13 Formas normales y cláusulas

13.1 Formas prenexas

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

13.2 Formas de Skolem . . . . . . . . . . . . . . . . . . . . . . . .

13.3 Formas clausales

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

14 Cláusulas

14.1 Cláusulas

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

14.2 Cláusulas y fórmulas . . . . . . . . . . . . . . . . . . . . . .

15 Teorema de Herbrand

15.1 Modelos de Herbrand . . . . . . . . . . . . . . . . . . . . . .

15.2 Teorema de Herbrand . . . . . . . . . . . . . . . . . . . . . .

15.3 Métodos de deducción basados directamente en el teorema
de Herbrand . . . . . . . . . . . . . . . . . . . . . . . . . . .

15.4 Resolución básica . . . . . . . . . . . . . . . . . . . . . . . .

16 Sustitución y unificación

16.1 Comparación de términos

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

16.2 Comparación de sustituciones . . . . . . . . . . . . . . . . .

16.3 Unificación . . . . . . . . . . . . . . . . . . . . . . . . . . . .

16.4 Unificación para fórmulas atómicas

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

17 Resolución en lógica de primer orden

17.1 Sistema de resolución . . . . . . . . . . . . . . . . . . . . . .

17.2 Corrección y completitud de la resolución . . . . . . . . . . .

17.3 Reglas de simplificación . . . . . . . . . . . . . . . . . . . .

17.4 Refinamientos de resolución . . . . . . . . . . . . . . . . . .

18 Programas lógicos: semántica declarativa

18.1 Programas lógicos . . . . . . . . . . . . . . . . . . . . . . . .

18.2 Modelos de Herbrand . . . . . . . . . . . . . . . . . . . . . .

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

66

66

66

68

69

69

71

74

74

76

77

78

79

79

82

83

86

88

88

90

90

91

92

92

94

96

4

19.1 Operadores y sus puntos fijos

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

19.2 El operador de consecuencia inmediata . . . . . . . . . . . .

20 Programas lógicos: semántica procedural

96

99

101

20.1 Proceso de computación: La resolución SLD . . . . . . . . . 101

20.2 Correción de la resolución SLD . . . . . . . . . . . . . . . . 103

20.3 Completitud de la resolución SLD . . . . . . . . . . . . . . . 103

20.4 Reglas de computación . . . . . . . . . . . . . . . . . . . . . 105
20.5 Árboles SLD . . . . . . . . . . . . . . . . . . . . . . . . . . . 106

20.6 Procedimientos de refutación. La evaluación de Prolog . . . 110

Bibliografía

111

5

Capítulo 1

Preliminares

1.1 Cadenas

Definición 1.1.1 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.

Definición 1.1.2 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) =

Lema 1.1.3

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

6

2. La concatenación es asociativa.

3. La concatenación no es conmutativa.

Nota 1.1.4 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).
Definición 1.1.5 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

Nota 1.2.1 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.

Definición 1.2.2 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 .



Definición 1.2.3 La clausura transitiva de X es

X + =

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

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

7

Definición 1.2.5

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

= X

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

2. El conjunto engendrado por X mediante F es



i≥0

X+ =

Xi

Lema 1.2.6 X + = X+

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

Definición 1.2.8 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.

+

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

Lema 1.2.10 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

i−1, entonces f (x1, . . . , xn) /∈

Xi.

2. Xi−1 = Xi.

Teorema 1.2.11 (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.

8

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 ).

9

Capítulo 2

Sintaxis de la lógica
proposicional

2.1 El lenguaje de la lógica proposicional

Definición 2.1.1 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 “)”.

Definición 2.1.2 El conjunto P ROP de las fórmulas (proposicionales)
0 → Σ∗
es el conjunto engendrado por SP mediante las aplicaciones C¬ : Σ∗
y C∨ : Σ∗

0 definidas por:

0

0 × Σ∗

0 → Σ∗

C¬(F ) = ¬F
C∨(F, G) = (F ∨ G)

Lema 2.1.3 (Principio de inducción para fórmulas)
Sea S ⊆ P ROP tal que:

1. SP ⊆ S;
2. si F ∈ S, ent