Lógica para las Ciencias Informáticas

2013

Lógica para las

Ciencias Informáticas
Resolución en P

Licenciatura en Sistemas

Dr. Carlos E. Alvez

[email protected]
Adaptación de: Simari - 2006 - UNS

Resolventes

 Para poder calcular resolventes en P debemos

extender la idea de resolvente básica que fue dada
para L.

 En particular, es necesario generalizar la

definición de resolvente para lograr calcular
resolventes en P.

 Fundamentalmente, para esto es necesario definir

como calcular resolventes entre cláusulas no
básicas.

1
Lógica para las Ciencias Informáticas
2013

Resolventes

 Como veremos, la definición de resolvente para

cláusulas arbitrarias es una definición general que
no requiere especificar como se encuentra el
unificador más general.

 Sin embargo, para encontrar el unificador más

general es posible utilizar el procedimiento de
cálculo de substituciones unificadoras más
generales, o unificador más general, introducido
como Procedimiento de Unificación de Robinson.

Definición de Resolvente
Def: Una resolvente de dos cláusulas arbitrarias C1 y C2 es
una tercera cláusula C3 obtenida de acuerdo al
siguiente procedimiento:
1. Si w1, w2,..., wm son las variables en C2 y la variable de
mayor índice que aparece en C1  C2 de acuerdo al
orden lexicográfico es xk, sea  la siguiente
substitución:
  [(xk+1,w1), (xk+2,w2), ..., (xk+m,wm) ]
Esta substitución es un renombre de variables de
manera tal que luego de aplicarla a C2 ninguna de las
variables que aparecen en C2 aparece en C1.
Este proceso se describe como separación estándar de
variables.
4

2
Lógica para las Ciencias Informáticas
2013

Definición de Resolvente (cont.)

2. Si existe un par de conjuntos de literales
L = { L1, L2, ..., Lr }  C1 y
M = { M1, M2, ..., Ms}  C2
tales que el conjunto
L  M = { L1, L2, ..., Lr, M1, M2, ..., Ms }
es unificable con unificador más general .
Entonces, L y M son literales complementarios (de
hecho ambos son conjuntos con un solo elemento, y
esos elementos son literales complementarios).
Así, C3 es el conjunto de literales (i.e. cláusula):
(C1 – L)  (C2 – M)
5

Resolventes (Ejemplo)
Sean C1 = { p(x1), p(f(x2)), p(f(a)), q(x2) } y
C2 = {p(x1), p(x2), r(x3) } tenemos:
 = [(xk+1,x1), (xk+2,x2), (xk+3,x3) ] dado que la variable de mayor índice en
C1  C2 es x3, con k = 3 obtenemos
 = [(x4,x1), (x5,x2), (x6,x3) ] y C2  = {p(x4), p(x5), r(x6) }
L ={ p(x1), p(f(x2)), p(f(a)) }  C1 y M ={p(x4), p(x5) }  C2
L  M = {p(x1), p(f(x2)), p(f(a)), p(x4), p(x5) }
es unificable por:
 = [(f(a), x1), (f(a), x4), (f(a), x5), (a, x2)]
y aplicando la definición
(C1 – { p(x1), p(f(x2)), p(f(a)) })   (C2 – {p(x1), p(x2) })   =
{ q(x2) }  { r(x3) }  = { q(x2) }  { r(x6) } =
{ q(a) }  { r(x6) } = { q(a), r(x6) } que es una resolvente.
6

3
Lógica para las Ciencias Informáticas
2013

Resolventes
Obs: Cualquier par de cláusulas tiene a lo sumo un número
finito de resolventes dado que existe solo un número
finito de pares L y M. Para cada uno de esos pares existe
a lo sumo una substitución más general  que los unifica.
 Una deducción por resolución se define como en el
Cálculo Proposicional reemplazando el término
resolvente fija por resolvente.

Lema: Dado un conjunto de cláusulas S, existirá una


refutación de S (S  ) si y solo si   n(S) para algún
n, donde  se define como antes:
n

0(S) = S
n+1(S) = (n (S))
7

Resolución (Ejemplos)
Por ejemplo:

q(x)  p(a) r(y)  p(a)

q(x)  r(y)

Con substitución 

4
Lógica para las Ciencias Informáticas
2013

Resolución (Ejemplos)

Por ejemplo:

q(x)  p(x) r(y)  p(a)

q(a)  r(y)

Con substitución a/x

Resolución (Ejemplos)

Por ejemplo:

q(x)  p(f(x)) r(y)  p(f(f(a)))

q(f(a))  r(y)

Con substitución f(a)/x

10

5
Lógica para las Ciencias Informáticas
2013

Refutación (Ejemplo)

1. p(x, e, x)
2. p(y, z, v)  p(y, v, w)  p(e, z, w)
3. p(a, f(u, v), e)
4. p(e, f(f(b, c), a), a)

5. p(x, z, e)  p(e, z, x) [ 1, 2 con x/y, e/v, x/w ]

6. p(e, f(u, v), a) [ 3, 5 con a/x, f(u,v)/z ]
7.  [ 4, 6 con f(b,c)/u, a/ v ]

11

Refutación (Ejemplo)
1. p(x,e,x) 2. p(y, z, v)  p(y,v,w)  p(e,z,w)

5. p(x, z, e)  p(e,z,x) [ 1, 2 con x/y, e/v, x/w ]

3. p(a,f(u,v),e)

6. p(e, f(u, v), a) [ 3, 5 con a/x, f(u,v)/z ]

4. p(e, f(f(b,c),a), a)

7.  [ 4, 6 con f(b,c)/u, a/ v ]

12

6
Lógica para las Ciencias Informáticas
2013

Ejemplo (Programa)
1. q(b, y).
2. q(x, e).
3. r(a, f(u, v)).
4. p(x, z, y)  r(y, z), q(y, x).
?- p(e, f(b, c), a). (consulta)
Usando “” para unificación, el proceso es el siguiente:
 Para responder a la consulta por p(e, f(b, c), a) el
intérprete busca una regla en el programa cuya
cabeza sea unificable con ella.
 La primera condición es que involucren el mismo
predicado.
13

Ejemplo (Programa)
1. q(b, y).
2. q(x, e).
3. r(a, f(u, v)).
4. p(x, z, y)  r(y, z), q(y, x).
?- p(e, f(b, c), a). (consulta)
 Es decir, la regla 4 es la única y debemos verificar si
p(x, z, y)  p(e, f(b, c), a) (el “” es unificación)
 esto es, tienen el mismo predicado y además:
x  e, z  f(b, c), y  a
 La primera unificación es posible con e/x, la
segunda con f(b, c)/z y la tercera con a/y.
14

7
Lógica para las Ciencias Informáticas
2013

Ejemplo (Programa)
1. q(b, y).
2. q(x, e).
3. r(a, f(u, v)).
4. p(x, z, y)  r(y, z), q(y, x).
?- p(e, f(b, c), a). (consulta)
 Al realizar las substituciones, e/x, f(b, c)/z, a/y en 4
obtenemos la regla
p(e, f(b, c), a)  r(a, f(b, c)), q(a, e).

 Que estipula que tendremos la cabeza si las consultas

del cuerpo tienen éxito, i.e. r(a, f(b, c)) y q(a, e) tienen
éxito.
15

Ejemplo (Programa)
1. q(b, y).
2. q(x, e).
3. r(a, f(u, v)).
4. p(x, z, y)  r(y, z), q(y, x).
?- p(e, f(b, c), a). (consulta)
 Para responder a la consulta r(a, f(b, c)) el intérprete
encuentra la regla 3 : r(a, f(u, v))
 Para que la respuesta sea afirmativa debe ser posible
r(a, f(b, c))  r(a, f(u, v)),
 es decir a  a, f(b, c)  f(u, v), además debe
poderse b  u, c  v, lo que es claramente posible.
 Resta responder la consulta q(a, e). 16

8
Lógica para las Ciencias Informáticas
2013

Ejemplo (Programa)
1. q(b, y).
2. q(x, e).
3. r(a, f(u, v)).
4. p(x, z, y)  r(y, z), q(y, x).
?- p(e, f(b, c), a). (consulta)
 Para responder a la consulta q(a, e) el intérprete primero
localiza la regla 1, q(b, y) con el mismo predicado pero
como b  a resulta que q(a, e)  q(b, y) y el intérprete
trata de localizar otra regla.
 Localiza la regla 2: q(x, e) y prueba si q(a, e)  q(x, e)
 Luego debemos verificar si x  a, e  e.
 Esto es posible y la consulta inicial tiene éxito.
17

Resolución
 DEF: Una derivación por resolución de una cláusula C a
partir de un conjunto de cláusulas S (denominadas cláusulas
input) es una secuencia de cláusulas C1, C2, ..., Cn tal que:
1. Cn es C
2. Para cada i, 1  i  n, Ci es o bien
a. un elemento de S, o bien
b. una resolvente entre Cm y Ck, donde m, k  i
La derivación es finita o infinita de acuerdo a la longitud de
la secuencia.

 DEF: Una deducción por resolución de la cláusula  a partir

de un conjunto de cláusulas S se denomina refutación.

18

9
Lógica para las Ciencias Informáticas
2013

Resolución

 Notación: Si C es una resolvente de un par de cláusulas en un

conjunto S, escribiremos S  C.

Escribiremos S  C si existe una deducción por resolución de C a
partir de S.

Escribiremos S   si existe una refutación a partir de S.

 Por ejemplo:

{ p(a), p(x) q(x), p(x) r(f(x)), q(a) r(f(a)) }  p(a) q(a)

 q(a)
{ p(a), p(x) q(x), p(x) r(f(x)), q(a) r(f(a)) } 

{ p(a), p(x) q(x), p(x) r(f(x)), q(a) r(f(a)) }  

19

Resolución

 Def: Dado un conjunto de cláusulas S, definimos (S)

como la unión de S con el conjunto de todas las
resolventes calculadas a partir de cláusulas de S, i.e.
(S)  S  { C : C es resolvente de C1 y C2
donde C1, C2  S }
(S) se denomina también la resolución de S.

 Def: Dado un conjunto de cláusulas S, definimos n(S), la

n-ésima resolución de S, de forma inductiva como sigue:
0(S) S
n+1(S)  (n (S))

20

10
Lógica para las Ciencias Informáticas
2013

Resolución
 Obs: Resulta claro a partir de la definición de 
que para cualquier S vale que S  (S)
De allí resulta que la aplicación reiterada y
sucesiva del operador  produce una secuencia
creciente, en el sentido de la inclusión de
conjuntos:
S = 0(S)  1(S)  2(S)  ...  n(S)
 Teo: Dado un conjunto finito de cláusulas S,

existirá una refutación S   si y solo si  
 (S) para algún n.
n

21

Universo de Herbrand

Def: Dado un conjunto de cláusulas S, definimos el

Universo de Herbrand de S (o también Dominio de
Herbrand) como el conjunto de términos HS obtenido a
partir de S de la siguiente manera:
1. Si a es una constante que aparece en S entonces
a pertenece a HS . Si S no contuviera constantes se
agrega una arbitraria.
2. Si t1, t2, …,tn son términos en HS y fkn es una letra
funcional n-aria que aparece en S entonces
fkn( t1, t2, …,tn ) pertenece a HS.

22

11
Lógica para las Ciencias Informáticas
2013

Universo de Herbrand (Ejemplos)

1. Sea S = { p(a) }, entonces el Universo de

Herbrand de S es HS = { a }
2. Sea S = { p(x) }, entonces HS = { a } para alguna
constante arbitraria a.
3. Sea S = { p(x, f(a)) }, entonces
HS = { a, f(a), f(f(a)), f(f(f(a))), … }
4. Sea S = { p(x, f(a)), r(g(y)) }, entonces
HS = { a, f(a), f(f(a)), f(f(f(a))), …, g(a), g(g(a)),
g(g(g(a))), …, f(g(a)), g(f(a)), g(f(g(a))), … }

23

Base de Herbrand

 Def: Dado un conjunto de cláusulas S,

definimos la Base de Herbrand de S, denotada
BS, como el conjunto de literales siguiente:

BS = { pkn( t1, t2, …,tn ) | pkn es una letra

predicativa n-aria que  S y t1, t2, …, tn
son términos en HS }

24

12
Lógica para las Ciencias Informáticas
2013

Base de Herbrand (Ejemplos)

1. Sea S = { p(x, y), r(y) }, entonces el Universo de

Herbrand de S es:
HS = { a } (una constante arbitraria)
y la Base de Herbrand será:
BS = { p(a, a), r(a) }
2. Sea S = { p(x, a), r(b) }, entonces el Universo de
Herbrand de S es:
HS = { a, b }
y la Base de Herbrand será:
BS = { p(a, a), p(b, a), p(a, b), p(b, b), r(a), r(b) }

25

Base de Herbrand (Ejemplos)

3. Sea S = { p(x, f(a)), r(g(y)) }, entonces el Universo

de Herbrand de S es

HS = { a, f(a), f(f(a)), f(f(f(a))), …, g(a), g(g(a)),

g(g(g(a))), …, f(g(a)), g(f(a)), g(f(g(a))), … }

y la Base de Herbrand será:

BS = { p(a, a), p(f(a), a), p(g(a), a), p(f(f(a)), a),

p(g(g(a)), a), …, r(a), r(f(a)), r(g(a)), … }

26

13
Lógica para las Ciencias Informáticas
2013

Saturación

 Def: Dado un conjunto de cláusulas S, y un conjunto P

de términos fijos, entonces la saturación de S sobre P,
denotado P((S)), es el conjunto que contiene a todas
las cláusulas fijas (ground) que es posible obtener a
partir de los elementos de S en los que se reemplazan
las variables con los términos que son miembros de P.

 Obs: Notemos que este reemplazo debe ser

consistente, i.e. las apariciones de la misma variable
en una cláusula se reemplazan por el mismo término.

27

Saturación (ejemplos)

1. Sea S = { p(x, a), r(y) }, y P = { a }

La saturación de S sobre P, es
P((S)) = { p(a, a), r(a) }

2. Sea S = { p(x, a), r(y) }, y P = { f(a) }

La saturación de S sobre P, es
P((S)) = { p(f(a), a), r(f(a)) }

28

14
Lógica para las Ciencias Informáticas
2013

Saturación (ejemplos)

3. Sea S = { p(x, a), r(y) }, y P = { a, f(a) }

La saturación de S sobre P, es
P((S)) = { p(a, a), p(f(a), a), r(a), r(f(a))}

4. Sea S = { p(x, a), r(y) }, y P = { a, b }

La saturación de S sobre P, es
P((S)) = { p(a, a), p(b, a), r(a), r(b)}

29

Expansión de Herbrand

 Def: Dado un conjunto de cláusulas S, y HS su

universo de Herbrand, entonces la saturación de
S por HS, es decir HS((S)), se denomina la
Expansión de Herbrand de S.

 Ejercicio: Dar un conjunto S de cláusulas tal que

la Base de Herbrand y la Expansión de
Herbrand sean distintas.

30

15
Lógica para las Ciencias Informáticas
2013

Teorema de Herbrand
 Teorema (Herbrand): Sea S un conjunto finito de
cláusulas, y HS su universo de Herbrand entonces S es
insatisfacible si y solo si algún subconjunto finito de
HS((S)) es inconsistente.

 Obs: En términos computacionales este teorema sugiere

un método para verificar la satisfabilidad de un conjunto
de cláusulas. Es posible generar de manera parcial, por
iteración de , el universo de Herbrand y realizar las
correspondientes substituciones para obtener parte de la
expansión de Herbrand, si fuera inconsistente entonces S
sería insatisfacible.

31

Procedimiento de Refutación

Dado el teorema siguiente (ya enunciado con anterioridad)

 Teo: Dado un conjunto finito de cláusulas S, existirá una

refutación S   si y solo si   n(S) para algún n.
El resultado siguiente es evidente:
 Teo: Un conjunto finito de cláusulas S es insatisfacible si
y solo si existe una refutación de S.
 Obs: Este último teorema es un resultado de completitud
para un sistema lógico cuya única regla de inferencia es
el principio de resolución que hemos definido.

32

16
Lógica para las Ciencias Informáticas
2013

Procedimiento de Refutación

 Nuevamente, como en el Cálculo Proposicional, a

partir del teorema anterior podríamos generar la
secuencia:
S  0(S), (S), 2(S), ..., n(S), ...
y verificar si i(S) contiene  para algún i.
 La diferencia aquí es que no es posible asegurar que
la sucesión creciente i(S) tenga una cota superior y
por lo tanto no se puede demostrar que exista un
punto fijo para la aplicación de este operador.

33

Procedimiento de Refutación

p(a) q(a) r(f(a))

p(x)  q(x)
p(x)  r(f(x))
r(f(a)) q(a) 
p(a)  r(f(a)) p(a)
q(a)  r(f(a)) p(a)  q(a) r(f(a))

34

17
Lógica para las Ciencias Informáticas
2013

Procedimiento de Refutación
 Observando la generación de las cláusulas resolventes
vemos que existe ineficiencia, sin embargo es posible
encontrar una refutación más directa.
1. p(a) 1. p(a)
2. p(x)  q(x) 2. p(x)  q(x)
3. p(x)  r(f(x)) 3. p(x)  r(f(x))
4. q(a)  r(f(a)) 4. q(a)  r(f(a))
------------------ ------------------
5. q(a) (de 1 y 2) 5. q(a) (de 1 y 2)
6. p(a)  q(a) (de 3 y 4) 6. r(f(a)) (de 1 y 3)
------------------ ------------------
7. p(a) (de 5 y 6) 7. q(a) (de 4 y 6)
------------------ ------------------
8.  (de 1 y 7) 8.  (de 5 y 7) 35

Procedimiento de Refutación

 Por lo antes descripto, se tratarán el la

próxima clase:

 Principios útiles: que permiten eliminar literales

o cláusulas que no conducen a una refutación.

 Refinamientos: son criterios o procedimientos

que sirven como guía en la búsqueda de la
refutación.

36

18