PDF de programación - Deducción automática y programación lógica

Deducción automática y

programación lógica

José A. Alonso Jiménez

Área de ciencias de la computación e inteligencia artificial

Universidad de Sevilla

Sevilla, 12 de Septiembre de 1995

Contenido

1 Deducción automática proposicional

1.1 El método de Davis-Putnam . . . . . . . . . . . . . . . . . . .

1.1.1 Métodos de decisión basados en formas normales

. . .

1.1.2 Cláusulas

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

1.1.3 El algoritmo de Davis–Putnam . . . . . . . . . . . . .

1.2 Resolución proposicional

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

1.2.1

Sistema de reesolución . . . . . . . . . . . . . . . . . .

1

1

1

4

7

9

9

1.2.2 Validez y completitud de la resolución . . . . . . . . . 10

1.2.3 Algoritmos de resolución . . . . . . . . . . . . . . . . . 10

1.3 Estrategias de resolución . . . . . . . . . . . . . . . . . . . . . 11

1.3.1 Resolución semántica . . . . . . . . . . . . . . . . . . . 11

1.3.2 Resolución P1 y N1 . . . . . . . . . . . . . . . . . . . . 13

1.3.3 Resolución lineal

. . . . . . . . . . . . . . . . . . . . . 15

1.3.4 Resolución con soporte . . . . . . . . . . . . . . . . . . 17

1.3.5 Resolución unidad y por entradas . . . . . . . . . . . . 18

1.4 Resolución para cláusulas de Horn proposicionales . . . . . . . 20

1.4.1 Cláusulas de Horn . . . . . . . . . . . . . . . . . . . . 20

1.4.2 Resolución y cláusulas de Horn . . . . . . . . . . . . . 21

1.4.3 Resolución SLD . . . . . . . . . . . . . . . . . . . . . . 22

2 Deducción automática en lógica de primer orden

24

2.1 Cláusulas de primer orden . . . . . . . . . . . . . . . . . . . . 24

i

2.1.1 Cláusulas: sintaxis y semántica . . . . . . . . . . . . . 24

2.1.2 Cláusulas y fórmulas . . . . . . . . . . . . . . . . . . . 27

2.2 Métodos de deducción basados directamente en el teorema de

Herbrand . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

2.2.1 Teorema de Herbrand . . . . . . . . . . . . . . . . . . . 29

2.2.2 Métodos de deducción . . . . . . . . . . . . . . . . . . 31

2.3 Sustitución y unificación . . . . . . . . . . . . . . . . . . . . . 33

2.3.1 Comparación de términos

. . . . . . . . . . . . . . . . 33

2.3.2 Comparación de sustituciones . . . . . . . . . . . . . . 36

2.3.3 Unificación . . . . . . . . . . . . . . . . . . . . . . . . 37

2.3.4 Unificación para fórmulas atómicas . . . . . . . . . . . 40

2.4 Resolución en lógica de primer orden . . . . . . . . . . . . . . 41

2.4.1

Sistema de resolución . . . . . . . . . . . . . . . . . . . 41

2.4.2 Corrección y completitud de la resolución . . . . . . . . 43

2.4.3 Reglas de simplificación . . . . . . . . . . . . . . . . . 44

2.4.4 Estrategias de resolución . . . . . . . . . . . . . . . . . 44

3 Programación lógica

45

3.1 Programas lógicos: semántica declarativa . . . . . . . . . . . . 45

3.1.1 Programas lógicos . . . . . . . . . . . . . . . . . . . . . 45

3.1.2 Modelos de Herbrand . . . . . . . . . . . . . . . . . . . 47

3.2 Programas lógicos: semántica de puntos fijos . . . . . . . . . . 48

3.2.1 Operadores y sus puntos fijos

. . . . . . . . . . . . . . 48

3.2.2 El operador de consecuencia inmediata . . . . . . . . . 51

3.3 Programas lógicos: semántica procedimental

. . . . . . . . . . 52

3.3.1 Proceso de computación: La resolución SLD . . . . . . 52

3.3.2 Correción de la resolución SLD . . . . . . . . . . . . . 54

3.3.3 Completitud de la resolución SLD . . . . . . . . . . . . 55

3.3.4 Reglas de computación . . . . . . . . . . . . . . . . . . 56
Árboles SLD . . . . . . . . . . . . . . . . . . . . . . . 58

3.3.5

3.3.6 Procedimientos de refutación. La evaluación de Prolog

61

ii

Bibliografía

62

iii

Capítulo 1

Deducción automática
proposicional

1.1 El método de Davis-Putnam

1.1.1 Métodos de decisión basados en formas normales

Definición 1.1.1.1

1. Un literal es un símbolo proposicional o su negación.

2. Un literal es positivo si es un símbolo proposicional y negativo, en

caso contrario.

3. Usaremos la letra L (posiblemente con índices) para representar lit-

erales.

4. El complementario de un literal L es

¬p

p

L =

si L = p;
si L = ¬p;

5. Los literales L y L son complementarios si L = L.
6. Una cláusula conjuntiva (ó ∧–cláusula) C es una conjunción de un

conjunto finito de literales; i.e., C =

Li

n

i=1

1

7. Una cláusula disjuntiva (ó ∨–cláusula) D es una disyunción de un

conjunto finito de literales; i.e., D =

Li

n

i=1

8. Una fórmula F está en forma normal conjuntiva (FNC) si es una

conjunción de un conjunto de cláusulas disjuntivas; i.e.,

F =

Li,j



mi

n

i=1

j=1



mi

n





9. Una fórmula F está en forma normal disjuntiva (FND) si es una

disyunción de un conjunto de cláusulas conjuntivas; i.e.,

F =

Li,j

i=1

j=1

10. F es una forma normal conjuntiva de G si F está en forma normal

conjuntiva y F ≡ G.

11. F es una forma normal disjuntiva de G si F está en forma normal

disjuntiva y F ≡ G.

Teorema 1.1.1.2 Para cada fórmula F existe una fórmula G1 y una fórmula
G2 tal que G1 es una forma normal conjuntiva de F y G2 es una forma normal
disyuntiva de F .

Nota 1.1.1.3 (Algoritmo de normalización)

Entrada: Una fórmula F .

Salida: Una forma normal conjuntiva de F , G.

Procedimiento: Sustituir en F , mientras sea posible, las subfórmulas:

(G ↔ H)
(G → H)
¬¬G
¬(G ∨ H)
¬(G ∧ H)
(G1 ∨ (G2 ∧ G3))
((G1 ∧ G2) ∨ G3))

por ((G → H) ∧ (H → G))
por (¬G ∨ H)
por G
por (¬G ∧ ¬H)
por (¬G ∨ ¬H)
por ((G1 ∨ G2) ∧ (G1 ∨ G3))
por ((G1 ∨ G3) ∧ (G2 ∨ G3))

2

Nota 1.1.1.4 Intercambiando el papel de las conectivas ∨ y ∧ en el algo-
ritmo anterior se obtiene una forma normal disyuntiva de la fórmula.

Lema 1.1.1.5 Sean L1, . . . , Ln literales. Son equivalentes:

n
n

i=1

1.

2.

Li es una tautología.

Li es inconsistente

i=1

3. {L1, . . . , Ln} contiene un par de literales complementarios.

Teorema 1.1.1.6

1. Una fórmula en forma normal conjuntiva es una tautología syss cada

una de sus cláusulas disjuntivas es una tautología.

2. Una fórmula en forma normal disjuntiva es inconsistente syss cada una

de sus cláusulas conjuntivas es inconsistente.

Algoritmo 1.1.1.7 (de inconsistencia mediante FND)

Entrada: Una fórmula F .

Salida: Consistente, si F es consistente; Inconsistente, en caso con-

trario.

Procedimiento:

Sean G una forma normal disjuntiva de F

G1, . . . , Gn las ∧–cláusulas de G

Desde i = 1 hasta n

si en Gi no ocurren literales complementarios,

entonces devolver Consistente y parar.

Devolver Inconsistente y parar.

Algoritmo 1.1.1.8 (de validez mediante FNC)

Entrada: Una fórmula F

Salida: Tautologia, si F es una tautología; No-tautologia, en caso

contrario.

Procedimiento:

3

Sean G una forma normal conjuntiva de F

G1, . . . , Gn las ∨–cláusulas de G

Desde i = 1 hasta n

si en Gi ocurren literales complementarios,

entonces devolver No-tautologia y parar.

Devolver Tautologia y parar.

1.1.2 Cláusulas

Definición 1.1.2.1

1. Una cláusula es un conjunto finito de literales.
2. La cláusula vacía es el conjunto vacío y se representa por .

Nota 1.1.2.2 Usaremos las siguientes variables sintácticas:

1. L para literales.

2. C, D para cláusulas.

3. S para conjuntos de cláusulas.

Definición 1.1.2.3 Sea C una cláusula.

1. El conjunto de los literales positivos de C se representa por C+

2. El conjunto de los literales negativos de C se representa por C−

Definición 1.1.2.4 Sea v una valoración de verdad.



1. Para cada literal L,

v(L) =

2. Para cada cláusula C,

v(p),
1 − v(p),

si L = p;
si L = ¬p.

v(C) = 1 syss existe un L ∈ C tal que v(L) = 1

3. Para cada conjunto de cláusulas S,

v(S) = 1 syss para todo C ∈ S, v(C) = 1

4

Lema 1.1.2.5 Sea v una valoración.

1. v() = 0.
2. v(∅) = 1.

Nota 1.1.2.6 En lo que sigue, escribiremos v(L), v(C) ó v(S) en lugar de
v(L), v(C) ó v(S)

Definición 1.1.2.7 Sea v una valoración.

1. v es un modelo de C (ó C es válida en v), v |= C, si v(C) = 1.
2. v es un modelo de S (ó S es válida en v), v |= S, si v(S) = 1.

Definición 1.1.2.8

1. C (resp. S) es consistente si tiene un modelo. En caso contrario, es

inconsistente.

2. C es una tautología, |= C, si v(C) = 1 para toda valoración v.
3. C es consecuencia de S, S |= C, si v(C) = 1 para todos los modelos

v de S.

Lema 1.1.2.9 C es una tautología syss contiene un par de literales comple-
mentarios.

Nota 1.1.2.10

1. Si S ⊆ S y S es consistente, entonces S es consistente.
2. Si ∈ S, entonces S es inconsistente.

Definición 1.1.2.11

1. El conjunto de fórmulas correspondiente a la cláusula C = es



n

i=1

5

F orm(C) =

Li : C = {L1, . . . , Ln}



2. El conjunto de fórmulas correspondiente al conjunto de cláusulas C = ∅





n

es

F orm(S) =

Fi : S = {C1, . . . , Cn}, Fi ∈ F orm(Ci)

i=1

Lema 1.1.2.12

1. Si F, G ∈ F orm(C), entonces F ≡ G.
2. Si F, G ∈ F orm(S), entonces F ≡ G.

Definición 1.1.2.13

1. C y F son equivalentes, C ≡ F , si v(C) = ˆv(F ) para toda valoración

v.

2. S y F son equivalentes, S ≡ F , si v(S) = ˆv(F ) para toda valoración

v.

3. S y S son equivalentes, S ≡ S, si v(S) = v(S) para toda valo-

ración v.

Lema 1.1.2.14

1. Si F ∈ F orm(C), entonces C ≡ F .
2. Si F ∈ F orm(S), entonces S ≡ F .

Teorema 1.1.2.15 Para cada fórmula F existe un conjunto de cláusulas S
tal que S ≡ F .

Definición 1.1.2.16 Un conjunto de cláusulas S es una forma clausal de
la fórmula F si S ≡ F .

No