PDF de programación - Tema 7: Implementación en Prolog de la resolución

Programación lógica

Curso 2002–03

Tema 7: Implementación en

Prolog de la resolución

José A. Alonso Jiménez

Jose-Antonio.Alonso@cs.us.es
http://www.cs.us.es/∼jalonso

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

Universidad de Sevilla

PL 2002–03

CcIa

Implementación en Prolog de la resolución

7.1

Introducción a la resolución
x Reducción de consecuencia lógica a inconsistencia de conjunto de
u Sea S un conjunto de fórmulas y F una fórmula. Son equivalentes:

cláusulas

• S |= F
• S ∪ {¬F} es inconsistente
• Cláusulas(S ∪ {¬F}) es inconsistente

x Decisión de la inconsistencia de un conjunto de cláusulas
u El conjunto de cláusulas S es inconsistente syss la cláusula vacía es consecuencia

de S.

PL 2002–03

CcIa

Implementación en Prolog de la resolución

7.2

Introducción a la resolución
x Reglas de inferencia:
u Reglas habituales:

p → q,
p
q
p → q, ¬q
¬p
p → q,
p → r

{¬p, q},
{q}
{¬p, q},
{¬p}
{¬p, q},
{¬p, r}

{p}
{¬q}
{¬q, r}

Modus Ponens:

Modus Tollens:

Encadenamiento:

q → r
u Regla de resolución proposicional:
{p1, . . . , r, . . . , pm},
{p1, . . . , pm, q1, , . . . , qn}

{q1, . . . , ¬r, . . . , qn}

PL 2002–03

CcIa

Implementación en Prolog de la resolución

7.3

Regla de resolución proposicional
x Complementarios
u El complementario de un literal L es
si L = ¬p
p,
¬p, si L = p



L =

u complementario(+L1,-L2) se verifica si L2 es el complementario del literal L1.
u Def. de complementario:

complementario(-A, A) :- !.
complementario(A, -A).

PL 2002–03

CcIa

Implementación en Prolog de la resolución

7.4

Regla de resolución proposicional
x Resolventes
u La cláusula C es una resolvente de las cláusulas C1 y C2 si existe un literal L tal
que L ∈ C1, L ∈ C2 y C = (C1 − {L}) ∪ (C2 − {L}).
u resolvente(+C1,+C2,-C3) se verifica si C3 es una resolvente de las cláusulas C1 y C2.
u Ejemplos:

?- resolvente([q, -p],[p, -q],C).
?- resolvente([q, -p], [q, r], C).
?- resolvente([p],[-p],C).

u Def. de resolvente:

=> C = [p, -p] ; C = [q, -q] ; No
=> No
=> C = [] ; No

resolvente(C1,C2,C) :-

member(L1,C1),
complementario(L1,L2),
member(L2,C2),
delete(C1, L1, C1P),
delete(C2, L2, C2P),
append(C1P, C2P, C3),
sort(C3,C).

PL 2002–03

CcIa

Implementación en Prolog de la resolución

7.5

Demostraciones por resolución
x Definiciones
u Sea S un conjunto de cláusulas.
u La sucesión (C1, . . . , Cn) es una demostración por resolución de la cláusula C a
partir de S si C = Cn y para todo i ∈ {1, ..., n} se verifica una de las siguientes
condiciones:
· Ci ∈ S;
· existen j, k < i tales que Ci es una resolvente de Cj y Ck

por resolución de C a partir de S.

u La cláusula C es demostrable por resolución a partir de S si existe una demostración
u Una refutación por resolución de S es una demostración por resolución de la
u Se dice que S es refutable por resolución si existe una refutación por resolución a

cláusula vacía a partir de S.

partir de S.

PL 2002–03

CcIa

Implementación en Prolog de la resolución

7.6

Demostraciones por resolución
x Definiciones
u Sea S un conjunto de fórmulas.
u Una demostración por resolución de F a partir de S es una refutación por res-
olución de Cláusulas(S ∪ {¬F}).
u La fórmula F es demostrable por resolución a partir de S si existe una demostración
x Ejemplo:
u Demostración por resolución de p ∧ q a partir de {p ∨ q, p ↔ q}:

por resolución de F a partir de S.

Hipótesis
1 {p,q}
Hipótesis
2 {-p,q}
3 {p,-q}
Hipótesis
4 {-p,-q} Hipótesis
5 {q}
7 {-q}
8 {}

Resolvente de 1 y 2
Resolvente de 3 y 4
Resolvente de 5 y 7

x El cálculo por resolución es adecuado y completo.

PL 2002–03

CcIa

Implementación en Prolog de la resolución

7.7

Búsqueda elemental de refutación
x Reglas para determinar la inconsistencia del conjunto de cláusulas S:
u Si S contiene a la cláusula vacía, entonces S es inconsistente.
u Si S contiene dos cláusulas C1, C2 que tienen una resolvente que no pertenece a S,
entonces S es inconsistente syss S ∪ {C} es inconsistente.
u En otro caso, S es consistente.
x Búsqueda elemental de refutación:
u refutacion(+S,-R) se verifica si R es una refutación por resolución del conjunto de
u Ejemplo:

cláusulas S.

?- refutacion([[-p,-q],[p,q],[-p,q],[-q,p]],R).
R = [[p,-q],[q,-p],[p,q],[-p,-q],

[q,-q],[p,-p],[-p],[q],[p],[]]

?- refutacion([[p,q],[-p,q],[-q,p]],R).
No

PL 2002–03

CcIa

Implementación en Prolog de la resolución

7.8

Búsqueda elemental de refutación
u Ejemplo con traza de resolventes:

?- refutacion([[-p,-q],[p,q],[-p,q],[-q,p]],R).
[q, -q] resolvente de [-p, -q] y [p, q]
[p, -p] resolvente de [-p, -q] y [p, q]
[-p] resolvente de [-p, -q] y [q, -p]
[q] resolvente de [-p] y [p, q]
[p] resolvente de [q] y [p, -q]
[] resolvente de [p] y [-p]

R = [[p,-q],[q,-p],[p,q],[-p,-q],

[q,-q],[p,-p],[-p],[q],[p],[]]

PL 2002–03

CcIa

Implementación en Prolog de la resolución

7.9

Búsqueda elemental de refutación
u Def. de refutacion:

refutacion(S,R) :-

maplist(sort,S,S1),
refutacion_aux(S1,R).

refutacion_aux(S,R) :-

member([],S), !,
reverse(S,R).

refutacion_aux(S,R) :-

member(C1,S),
member(C2,S),
resolvente(C1,C2,C),
\+ member(C, S),
% format(’Ñ~w resolvente de ~w y ~wñ’, [C,C1,C2]),
refutacion_aux([C|S],R).

PL 2002–03

CcIa

Implementación en Prolog de la resolución

7.10

Búsqueda de refutación de OTTER
x Ejemplo de búsqueda de refutación con
u Entrada ejemplo.in

OTTER

list(sos).
-p | -q.
p | q.
-p | q.
-q | p.
end_of_list.

set(binary_res).
set(very_verbose). % Presentación detallada

% Resolución binaria

u Ejecución otter <ejemplo.in >ejemplo.out

PL 2002–03

CcIa

Implementación en Prolog de la resolución

7.11

Búsqueda de refutación de OTTER
u Fichero de salida ejemplo.out

list(sos).
1 [] -p| -q.
2 [] p|q.
3 [] -p|q.
4 [] -q|p.
end_of_list.

=========== start of search ===========
given clause #1: (wt=2) 1 [] -p| -q.

given clause #2: (wt=2) 2 [] p|q.

0 [binary,2.1,1.1] q| -q.
0 [binary,2.2,1.2] p| -p.

given clause #3: (wt=2) 3 [] -p|q.

0 [binary,3.1,2.1] q|q.

** KEPT (pick-wt=1): 5 [binary,3.1,2.1,factor_simp] q.

0 [binary,3.2,1.2] -p| -p.

** KEPT (pick-wt=1): 6 [binary,3.2,1.2,factor_simp] -p.

PL 2002–03

CcIa

Implementación en Prolog de la resolución

7.12

Búsqueda de refutación de OTTER

given clause #4: (wt=1) 5 [...] q.

0 [binary,5.1,1.2] -p.
Subsumed by 6.

given clause #5: (wt=1) 6 [...] -p.

0 [binary,6.1,2.1] q.
Subsumed by 5.

given clause #6: (wt=2) 4 [] -q|p.

0 [binary,4.1,5.1] p.

** KEPT (pick-wt=1): 7 [binary,4.1,5.1] p.

----> UNIT CONFLICT at

0.00 sec ----> 8 $F.

PL 2002–03

CcIa

Implementación en Prolog de la resolución

7.13

Búsqueda de refutación de OTTER

---------------- PROOF ----------------
1 [] -p| -q.
2 [] p|q.
3 [] -p|q.
4 [] -q|p.
5 [binary,3.1,2.1,factor_simp] q.
6 [binary,3.2,1.2,factor_simp] -p.
7 [binary,4.1,5.1] p.
8 [binary,7.1,6.1] $F.
------------ end of proof -------------

PL 2002–03

CcIa

Implementación en Prolog de la resolución

7.14

Búsqueda de refutación de OTTER
x Procedimiento de búsqueda de pruebas
u Mientras el soporte es no vacío y no se ha encontrado una refutación

1. Seleccionar como cláusula actual la cláusula menos pesada del soporte (i.e. con

el menor número de átomos).

2. Mover la cláusula actual del soporte a usable.

3. Calcular las resolventes de la cláusula actual con las cláusulas usables.

4. Procesar cada una de las resolventes calculadas anteriormente.

5. Añadir al soporte cada una de las cláusulas procesadas que supere el proce-

samiento.

PL 2002–03

CcIa

Implementación en Prolog de la resolución

7.15

Búsqueda de refutación de OTTER
u El procesamiento de cada una de resolventes consta de los siguientes pasos (los indicados con * son

opcionales):

*1. Escribir la resolvente.

*2. Aplicar a la resolvente eliminación unitaria (i.e. elimina los literales de la resolvente tales que

hay una cláusula unitaria complementaria en usable o en soporte).

3. Descartar la resolvente y salir si la resolvente es una tautología (i.e A y -A).

4. Descartar la resolvente y salir si la resolvente es subsumida por alguna cláusula de usable o del

soporte (subsunción hacia adelante).

5. Añadir la resolvente al soporte.

*6. Escribir la resolvente retenida.

7. Si la resolvente tiene 0 literales, se ha encontrado una refutación.

8. Si la resolvente tiene 1 literal, entonces buscar su complementaria (refutación) en usable y

soporte.

*9. Si se ha encontrado una refutación, escribirla.

*10. Descartar cada cláusula de usable o del soporte subsumida por la resolvente (subsunción hacia

atrás).

El paso 10 no se da hasta que los pasos 1–9 se han aplicado a todas las resolventes.

PL 2002–03

CcIa

Implementación en Prolog de la resolución

7.16

Refutación de conjuntos de cláusulas
x Procedimiento principal
u refutacion(+U,+S) se verifica si se existe una refutación con usables U y soporte S
u Ejemplos:

(además, escribe la búsqueda y la prueba).

?- refutacion([], [[p,q],[-p,q],[-q,p],[-p,-q]]).

Usable:

Soporte:
1 [] [p, q]
2 [] [-p, q]
3 [] [-q, p]
4 [] [-p, -q]

cláusula actual #1: 1 [] [p, q]

PL 2002–03

CcIa

Implementación en Prolog de la resolución

7.17

Refutación de conjuntos de cláusulas

cláusula actual #2: 2 [] [-p, q]

0 [2, 1] [q]

** RETENIDA: 5 [2, 1] [q]
5 subsume a 2
5 subsume a 1

cláusula actual #3: 5 [2, 1] [q]

cláusula actual #4: 3 [] [-q, p]

0 [3, 5] [p]

** RETENIDA: 6 [3, 5] [p]
6 subsume a 3

cláusula actual #5: 6 [3, 5] [p]

cláusula actual #6: 4 [] [-p, -q]

0 [4, 6] [-q]

** RETENIDA: 7 [4, 6] [-q]

----> CONFLICTO UNITARIO 8 [7,5] []

PL 2002–03

CcIa

Implementación en Prolog de la resolución

7.18

Refutación de conjuntos de cláusulas

---------------- DEMOSTRACION ----------------
1 [] [p, q]
2 [] [-p, q]
3 [] [-q, p]
4 [] [-p, -q]
5 [2, 1] [q]
6 [3, 5] [p]
7 [4, 6] [-q]
8 [7, 5] []
----------- fin de la demostración ----------