Resoluci on SLD y Prolog

Eduardo Bonelli
Departamento de Computacion, FCEyN, UBA
21 de octubre de 2008
Repaso de la clase pasada
Clausulas de Horn y resolucion en Prolog
Refutaciones como computaciones
Metodo de resolucion

Dado un conjunto de clausulas S

1. Aplicar repetidamente la regla de resolucion dando lugar a
pasos de resolucion
2. Hasta producir una refutacion (i.e. conjunto de clausulas
contieniendo una clausula vaca o contradiccion)

En este caso decimos que S tiene una refutacion por

resolucion

Sustento del metodo

Cada paso de resolucion preserva insatisfactibilidad
+ las refutaciones son trivialmente insatisfactibles
= refutacion por resolucion general de S implica que S es
insatisfactible
Regla de resoluci on
{B
1
, . . . , B
k
, A
1
, . . . , A
m
} {D
1
, . . . , D
l
, C
1
, . . . , C
n
}
({A
1
, . . . , A
m
, C
1
, . . . , C
n
})
donde es el MGU de {B
1
, . . . , B
k
, D
1
, . . . , D
l
}.

Asumimos que las clausulas {B

1
, . . . , B
k
, A
1
, . . . , A
m
} y
{D
1
, . . . , D
l
, C
1
, . . . , C
n
} no tienen variables en com un; en
caso contrario se renombran las variables

Observar que (B
1
) = . . . = (B
k
) = (D
1
) = . . . = (D
l
)

La clausula ({A
1
, . . . , A
m
, B
1
, . . . , B
n
}) se llama resolvente
(de {B
1
, . . . , B
k
, A
1
, . . . , A
m
} y {D
1
, . . . , D
l
, C
1
, . . . , C
n
})
Resoluci on lineal

Si bien el metodo de resolucion general es completo, hallar

refutaciones es un proceso muy caro en el caso general

El espacio de b usqueda producido puede ser enorme

Hay un alto grado de no-determinismo

Que clausulas elegimos? Regla de b usqueda

Que literales eliminamos? Regla de seleccion

Se precisan restricciones (regla de b usqueda y seleccion) para

reducir el espacio de b usqueda (utilidad practica)

Es deseable que dichas restricciones no renuncien a la

completitud del metodo
Resoluci on lineal
Una secuencia de pasos de resolucion a partir de S es lineal si es de
la forma:
B
1
T
T
T
T
T
T
T
T
T C
0
B
2
T
T
T
T
T
T
T
T
T C
1

1
B
3
T
T
T
T
T
T
T
T
T C
2

2
C
3

3
B
p1
S
S
S
S
S
S
S
. . .
B
p
S
S
S
S
S
S
S
C
p1

p1
C
p
=

p
donde C
0
y cada B
i
es un elemento de S o alg un C
j
con j < i
Resoluci on lineal

En general, reduce el espacio de b usqueda considerablemente

Preserva completitud

Sin embargo sigue siendo altamente no-determinstico

El criterio de b usqueda deja espacio para renamientos

No se especico ning un criterio de seleccion

Clausulas de Horn

Mayor eciencia en el proceso de producir refutaciones sin

perder completitud puede lograrse para subclases de formulas

Una de estas clases es la de Clausulas de Horn

Una clausula de Horn es una disyuncion de literales que tiene

a lo sumo un literal positivo

Para conjuntos de clausulas de Horn puede usarse una

variante de resolucion lineal, llamada resolucion SLD, que
goza de buenas propiedades
Repaso de la clase pasada
Clausulas de Horn y resolucion en Prolog
Clausulas de Horn y resolucion SLD
Resolucion SLD en Prolog
Refutaciones como computaciones
Forma clausal
Conjuncion de sentencias prenexas de la forma x
1
. . . x
m
C donde
1. C es una disyuncion de literales y
2. los conjuntos {x
1
, . . . , x
m
} de variables ligadas son disjuntos
para todo par distinto de clausulas.
Nota:

Cada x
1
. . . x
m
C se llama clausula

La forma clausal
x
11
. . . x
1m
1
C
1
. . . x
k1
. . . x
km
k
C
k
se escribe {C

1
, . . . , C

k
} donde C

i
resulta de reemplazar la
disyuncion de literales C
i
por el conjunto de literales asociado
Clausulas de Horn
Una clausula x
1
. . . x
m
C tal que la disyuncion de literales C tiene
a lo sumo un literal positivo
Nota: C puede tomar una de las formas:

{B, A
1
, . . . , A
n
}

{B}

{A
1
, . . . , A
n
} (llamada clausula goal o negativa)
Relaci on con formulas de primer orden

No toda formula de primer orden puede expresarse como una

clausula de Horn
Ejemplo
x.P(x) Q(x)

Sin embargo, el conjunto de clausulas de Horn es

sucientemente expresivo para representar programas, en la
vision de resolucion como computacion

mas detalles por venir

Resoluci on SLD

Clausula de denicion (Denite Clause)

Clausula de la forma x
1
. . . x
m
C tal que la disyuncion de
literales C tiene exactamente un literal positivo

Sea S = P {G} un conjunto de clausulas de Horn (con

nombre de variables disjuntos) tal que

P conjunto de clausulas de denicion y

G un clausula negativa

S = P {G} son las clausulas de entrada

P se conoce como el programa o base de conocimientos y

G el goal o meta
Resoluci on SLD
Un secuencia de pasos de resolucion SLD para S es una secuencia
< N
0
, N
1
, . . . , N
p
>
de clausulas negativas que satisfacen las siguientes dos condiciones.
1. N
0
es el goal G
2. sigue en transparencia siguiente
Resoluci on SLD
2. para todo N
i
en la secuencia, 0 < i < p, si N
i
es
{A
1
, . . . , A
k1
, A
k
, A
k+1
, . . . , A
n
}
entonces hay alguna clausula de denicion C
i
de la forma
{A, B
1
, . . . , B
m
} en P tal que A
k
y A son unicables con MGU
, y si

m = 0, entonces N
i +1
es
{(A
1
, . . . , A
k1
, A
k+1
, . . . , A
n
)}

m > 0, entonces N
i +1
es
{(A
1
, . . . , A
k1
, B
1
, . . . , B
m
, A
k+1
, . . . , A
n
)}
Refutaci on SLD
Secuencia de pasos de resolucion SLD < N
0
, . . . , N
p
> tal que
N
p
=
C
1
T
T
T
T
T
T
T
T
T N
0
= G
C
2
T
T
T
T
T
T
T
T
T N
1

1
C
3
T
T
T
T
T
T
T
T
T N
2

2
N
3

3
C
p1
S
S
S
S
S
S
S
. . .
C
p
S
S
S
S
S
S
S
N
p1

p1
N
p
=

p
Sustituci on respuesta

En cada paso, las clausulas

{A
1
, . . . , A
k1
, A
k
, A
k+1
, . . . , A
n
} y
{A, B
1
, . . . , B
m
} son resueltas

No se especica regla de b usqueda alguna

Los atomos A
k
y A son unicados con MGU
i

El literal A
k
se llama atomo seleccionado de N
i

No se especica regla de seleccion alguna

Sustitucion respuesta es la sustitucion

p
. . .
1

se usa en Prolog para extraer la salida del programa

Ejemplo
Consideremos las siguientes clausulas de denicion

C
1
= {add(U, 0, U)}

C
2
= {add(X, succ(Y), succ(Z)), add(X, Y, Z)}
y la clausula goal G
{add(succ(0), V, succ(succ(0)))}

Deseamos mostrar que el conjunto de estas clausulas (i.e.

{C
1
, C
2
, G}) es insatisfactible

Contamos con la siguiente refutacion SLD

Ejemplo
Clausula goal Clausula de entrada Sust.
{add(succ(0), V, succ(succ(0)))} C
2
{add(succ(0), Y, succ(0))} C
1

1

2
donde

1
= {succ(0)/X, succ(0)/Z, succ(Y)/V}

2
= {succ(0)/U, 0/Y}

La sustitucion resultado es
{succ(0)/X, succ(0)/Z, succ(0)/V, succ(0)/U, 0/Y}
Correcci on y completitud
Correcci on
Si un conjunto de clausulas de Horn tiene una refutacion SLD,
entonces es insatisfactible
Completitud
Dado un conjunto de clausulas de Horn P {G} tal como se
describio, si P {G} es insatisfactible, existe una refutacion SLD
cuya primera clausula es G.
Repaso de la clase pasada
Clausulas de Horn y resolucion en Prolog
Clausulas de Horn y resolucion SLD
Resolucion SLD en Prolog
Refutaciones como computaciones
Resoluci on SLD en Prolog

Prolog utiliza resolucion SLD con las siguientes restricciones

Regla de b usqueda: se seleccionan las clausulas de programa

de arriba hacia abajo, en el orden en que fueron introducidas

Regla de seleccion: seleccionar el atomo de mas a la izquierda

La suma de regla de b usqueda y regla de seleccion se llama

estrategia

Cada estrategia determina un arbol de b usqueda o arbol SLD

Ejemplo
Clausulas de Def. Goal
{p(X, Z), q(X, Y), p(Y, Z)} {p(X, b)}
{p(X, X)}
{q(a, b)}
Ejemplo - arbol SLD
p(X, b)
1
.r
r
r
r
r
r
r
r
r
r
2

F
F
F
F
F
F
F
F
q(X, Y), p(Y, b)
3

({b/X})
p(b, b)
1
l
l
l
l
l
l
l
l
l
l
l
l
l
2

L
L
L
L
L
L
L
L
L
L
q(b, U), p(U, b)
falla

({a/X})
Variando la regla de seleccion

Si variamos la regla de seleccion, vara el arbol SLD asociado

Vamos a asumir ahora que la regla de selecci on es

seleccionar el de mas a la derecha
Ejemplo - atomo de mas la derecha
p(X, b)
1
.t
t
t
t
t
t
t
t
t
2

C
C
C
C
C
C
C
C
q(X, Y), p(Y, b)
1
.q
q
q
q
q
q
q
q
q
q
2

H
H
H
H
H
H
H
H
H
H
H

({b/X})
q(X, Y), q(Y, U),
p(U, b)
1
.r
r
r
r
r
r
r
r
r
r
2

K
K
K
K
K
K
K
K
K
K
K
q(X, b)
3

q(X, Y), q(Y, U),

q(U, V),p(V, b)
1
|
|
|
|
|
|
|
|
2

N
N
N
N
N
N
N
N
N
N
N
N
N
q(X, Y), q(Y, b)
3

({a/X})
q(X, a)
falla
Variando la regla de b usqueda

Si variamos la regla de b usqueda, tambien vara el arbol SLD

asociado

Ejercicio: asumir ahora que la regla de b usqueda es

seleccionar las clausulas de programa be abajo hacia arriba
y armar el arbol SLD del ejemplo
Repaso de la clase pasada
Clausulas de Horn y resolucion en Prolog
Refutaciones como computaciones
Introduccion
Cut y negacion
Motivaci on

En esta parte de la clase exploramos de que manera resolucion

SLD puede usarse para computar

Asimismo, vamos a enfatizar el rol de la sustitucion respuesta

como resultado de calculo
Motivaci on

Recordar el ejemplo de la suma

C
1
= {add(U, 0, U)}

C
2
= {add(X, succ(Y), succ(Z)), add(X, Y, Z)}

Estas clausulas pueden verse como una denicion recursiva de

la suma

Supongamos que queremos saber si, dada esa denicion,

V.add(succ(0), V, succ(succ(0)))

En otras palabras
Existe V tal que 1 + V = 2?
Motivaci on
Lo podemos plantear como la validez de la formula
C
1
C
2
V.add(succ(0), V, succ(succ(0)))
Es decir,
(U.C
1
X.Y.Z.C
2
)

Dene la suma

V.add(succ(0), V, succ(succ(0)))

Pide calcular V
es valida
Motivaci on
Esto es lo mismo que preguntarse por la insatisfactilidad de
C
1
C
2
V.add(succ(0), V, succ(succ(0)))
O lo que es lo mismo
C
1
C
2
V.add(succ(0), V, succ(succ(0)))
Resolucion SLD testea por insatisfactibilidad!
Motivaci on
Resolucion SLD se dispara a partir del conjunto de clausulas

{add(U, 0, U), {add(X, succ(Y), succ(Z)), add(X, Y, Z)}

{add(succ(0), V, succ(succ(0)))}

En caso de tener exito, va a hallar el V buscado

Importante observar que

No solamente interesa saber que existe tal V (i.e. que existe la

refutacion)

Ademas, queremos una instancia del mismo

La sustitucion respuesta proveera dichas instancias; las

mismas pueden interpretarse como el resultado del computo
Programas logicos - Notaci on Prolog
Recordar que la resolucion SLD parte de un conjunto de clausulas
S = P {G} donde
1. P es un conjunto de clausulas de denicion

Clausulas con exactamente un literal positivo

{B, A
1
, . . . , A
n
}
{B}
2. G es un goal

Clausula negativa
{A
1
, . . . , A
n
}
Notaci on Prolog para programas l ogicos
B A
1
. . . A
n
(A
1
. . . A
n
) B
(A
1
. . . A
n
) B
Como consecuencia, las clausulas en P se escriben

B : A
1
, . . . , A
n
para {B, A
1
, . . . , A
n
} (reglas)

B. para B (hechos)
Ejemplo de la suma en notaci on Prolog
Volviendo al ejemplo de la suma, el programa Prolog es
add(U,0,U).
add(X,succ(Y),succ(Z)):-add(X,Y,Z).
Ingresamos el goal
?- add(succ(0),V,succ(succ(0)))
La respuesta es:
V=succ(0)
Ejemplo I
padres(fred, sally).
padres(tina, sally).
padres(sally, john).
padres(sally, diane).
padres(sam, bill).
hermanos(A, B) :- padres(P, A), padres(P, B), A \== B.

Si el goal es hermanos(john,X) entonces la refutacion SLD

para P X.hermanos(john, X) arrojara la sustitucion
respuesta = {diane/X}

Nota: Puede que la sustitucion respuesta asigne valores a

variables intermedias (no exhibidas en ) que sugieron en el
proceso de b usqueda de una refutacion
Ejemplo II
Terminos de primer orden para representar estructuras de datos

mas(A,B) (suma)

menos(A,B) (resta)

por(A,B) (producto)
eval(mas(A,B),CV):-eval(A,AV),eval(B,BV),CV is AV+BV.
eval(menos(A,B),CV):-eval(A,AV),eval(B,BV),CV is AV-BV.
eval(por(A,B),CV):-eval(A,AV),eval(B,BV),CV is AV*BV.
eval(Num,Num):-number(Num).

Dado el goal eval(menos(mas(2,3),1),X) la sustitucion

resultado sera {4/X}
Correcci on y completitud
Correcci on
Si existe una refutacion SLD de P {G} con la estrategia antes
mencionada entonces es insatisfactible
Completitud
Si P {G} es insatisfactible, entonces una refutacion SLD con la
estrategia antes mencionada a partir del mismo
B usqueda de refutaciones SLD en Prolog

Recorre el arbol SLD en profundidad (depth-rst search)

La ventaja del recorrido en profundidad es que puede ser

implementado de manera muy eciente

Se usa una pila para representar los atomos del goal

Se hace un push del resolvente del atomo del tope de la pila

con la clausula de denicion

Se hace un pop cuando el atomo del tope de la pila no unica

con ninguna clausula de denicion mas (luego, el atomo que
queda en el tope se unica con la siguiente clausula de
denicion)

Desventaja: puede que no encuentre una refutacion SLD a un

si existe!
Repaso de la clase pasada
Clausulas de Horn y resolucion en Prolog
Refutaciones como computaciones
Introduccion
Cut y negacion
Mas sobre Prolog
Dos temas que de Prolog que no hemos desarrollado
1. Cut
2. Deduccion de informacion negativa
Cut

Es una anotacion que permite podar el arbol SLD

Es de caracter extra-logico (i.e. no se corresponde con un

predicado estandar de la logica)

Se encuentra presente por cuestiones de eciencia

Debe usarse con cuidado dado que puede podarse una rama
de exito
Ejemplo
?-member(Y,[[1,2],[3,4]]),member(X,Y).
% devuelve X=1,X=2,X=3,X=4 sucesivamente
?-member(Y,[[1,2],[3,4]]),member(X,Y),!.
% devuelve X=1 solamente
?-member(Y,[[1,2],[3,4]]),!,member(X,Y).
% devuelve X=1, X=2 sucesivamente
?-!,member(Y,[[1,2],[3,4]]),member(X,Y).
% devuelve X=1,X=2,X=3,X=4 sucesivamente
Ejemplo
p(a).
p(X) :- q(X), r(X).
p(X) :- u(X).
q(X) :- s(X).
r(a).
r(b).
s(a).
s(b).
s(c).
u(d).
?- p(X),!.
X=a ;
no
?- r(X),!,s(Y).
X=a Y=a ;
X=a Y=b ;
X=a Y=c ;
no
?- r(X), s(Y), !.
X=a Y=a ;
no
Ejemplo

Denicion de max
max(X,Y,Y) :- X =< Y.
max(X,Y,X) :- X>Y.

Es ineciente. Por que? Pensar en max(3,4,Z)...

Mejor as
max(X,Y,Y) :- X =< Y, !.
max(X,Y,X) :- X>Y.

Y esto?
max(X,Y,Y) :- X =< Y, !.
max(X,Y,X).

Cambia la semantica de max

Probar max(2,3,2)
Cut - En general

Cuando se selecciona un cut, tiene exito inmediatamente

Si, debido a backtracking, se vuelve a este cut, su efecto es el

de hacer fallar el goal que le dio origen

El goal que unico con la cabeza de la cl uasula que contiene al

corte y que hizo que esa clausula se activara

El efecto obtenido es el de forzar determinismo (i.e. a lo sumo

una solucion) de
1. el goal pariente
2. cualquier goal que ocurre a la izquierda del corte en la clausula
que contiene el corte
3. todos los subgoals que se ejecutaron durante la ejecucion de
los goals precedentes
Negaci on por falla

Se dice que un arbol SLD falla nitamente si es nito y no

tiene ramas de exito

Dado un programa P el conjunto de falla nita de P es

{B | B atomo ground y existe un arbol SLD que falla
nitamente con B como raz}
Negation as failure
B atomo ground B en conjunto de falla nita de P
B
Predicado not
Negacion por falla en Prolog
not(G) :- G, !, fail.
not(G).
Ejemplo
Puede deducirse not(student(mary)) a partir de
student(joe).
student(bill).
student(jim).
teacher(mary).
Negaci on por falla no es negacion logica
hombre(juan).
hombre(pedro).
mujer(X) :- not(hombre(X)).

El query mujer(juan) da no, tal como se espera

El query mujer(X) da s, tal como se espera

Resultado del query mujer(X) ? (i.e. X.mujer (X))

Es importante que el predicado del not sea ground

Negaci on por falla no es negacion logica
hombre(juan).
hombre(pedro).
mujer(X) :- not(hombre(X)).
not(G) :- G, !, fail.
not(G).

Observar: el goal not(G) nunca instancia variables de G

Si G tiene exito, fail falla y descarta la sustitucion

Caso contrario, not(G) tiene exito inmediatamente (sin afectar

G)

En consecuencia, not(not(hombre(X))) no es equivalente a

hombre(X)
Negaci on por falla no es negacion logica
firefighter_candidate(X) :-
not( pyromaniac(X) ),
punctual(X).
pyromaniac(attila).
punctual(jeanne_d_arc).

Resultado del query firefighter_candidate(W)?

Por que jeanne_d_arc no es solucion?

Despues de todo: Si se intercambian las dos clausulas en la

denicion de firefighter_candidate s da a
jeanne_d_arc como solucion!

Es importante que el predicado del not sea ground