Post on 29-Jan-2016
description
TEMA 5
Resolucion
5.1. Interpretaciones de Herbrand
En la definicion de la teorıa de modelos para la Logica de Primer Orden,
necesitamos utilizar dominios que contengan mas elementos que constantes
tiene el lenguaje. Hemos vistos varios ejemplos en los que se muestra la nece-
sidad de tal condicion; en particular, si el conjunto de las constantes es vacıo,
ya que los dominios no pueden ser vacıos.
Sin embargo, para determinadas familias de formulas, es posible caracteri-
zar la satisfacibilidad a partir de interpretaciones construidas sobre el conjunto
de constantes. Las formulas en forma normal de Skolem tienen esta propiedad.
5.1.1. Forma normal de Skolem
Definicion 5.1 Una formula de un lenguaje de primer orden se dice que
esta en forma normal prenexa si responde al esquema
Q1x1 . . .QnxnA(x1, . . . , xn),
en donde Qi ∈ ∀,∃ y la formula A no contiene cuantificadores. La secuencia
Q1x1 . . .Qnxn se denomina prefijo y la formula A se denomina matriz.
Las equivalencias basicas de la Logica de Primer Orden demuestran que
podemos extraer los cuantificadores en una formula cualquiera y obtener una
formula equivalente.
Teorema 5.2 Toda formula de la Logica de Primer Orden es equivalente a
una formula en forma normal prenexa.
I. T. en Informatica de Sistemas. Logica computacional 1
2 Logica Computacional
Ejemplo 5.1.1
∀x(∃xP (x) → ∃yQ(x, y)) ≡ ∀z(∃xP (x) → ∃yQ(z, y)) (5.1)
≡ ∀z∃y(∃xP (x) → Q(z, y)) (5.2)
≡ ∀z∃y∀x(P (x) → Q(z, y)) (5.3)
Para poder extraer el cuantificador ∃x, necesitamos que la variable x no sea li-
bre en el consecuente de la implicacion. Dado que esto no ocurre en la formula
inicial, necesitamos renombrar una de las variables x; esto lo hacemos en (5.1).
En el paso (5.2) extraemos el cuantificador del consecuente de la implicacion
y en (5.3) extraemos el cuantificador del antecedente; observese que en este
caso, cambia el tipo de cuantificador.
La formula en forma normal prenexa equivalente a una dada, no es unica.
Aparte de las distintas equivalencias que nos permiten transformar la matriz,
tambien podemos obtener distintos prefijos segun el orden que sigamos para
extraer los cuantificadores.
Ejemplo 5.1.2 La formula del ejemplo 5.1.1 puede convertirse en forma nor-
mal prenexa de otras formas:
∀x(∃xP (x) → ∃yQ(x, y)) ≡ ∀z(∃xP (x) → ∃yQ(z, y))
≡ ∀z∀x(P (x) → ∃yQ(z, y))
≡ ∀z∀x∃y(P (x) → Q(z, y))
Aquı hemos extraido en primer lugar el cuantificador del antecedente y despues
el cuantificador del consecuente.
∀x(∃xP (x) → ∃yQ(x, y)) ≡ ∀z(∃xP (x) → ∃yQ(z, y))
≡ ∃xP (x) → ∀z∃yQ(z, y)
≡ ∀x(P (x) → ∀z∃yQ(z, y))
≡ ∀x∀z(P (x) → ∃yQ(z, y))
≡ ∀x∀z∃y(P (x) → Q(z, y))
En este ultimo, hemos introducido primero el cuantificador hasta el consecuen-
te y despues hemos extraido los tres.
Tal y como veremos mas adelante, de las tres opciones, la mejor sera la
que hemos obtenido en el ejemplo 5.1.1.
Definicion 5.3 Una formula esta en forma normal de Skolem si esta en
forma normal prenexa y en su prefijo no aparecen cuantificadores existenciales.
E.T.S.I.Informatica
Tema 5: Resolucion. 3
A diferencia de las formas normales que hemos estudiado hasta ahora, no
es posible, en general, obtener una formula en forma normal de Skolem que
sea equivalente a una formula dada. Sin embargo, sı podemos obtener una
propiedad mas debil, pero que sera suficiente para nuestros objetivos: siempre
podemos obtener una formula equisatisfacible y en forma normal de Skolem.
Teorema 5.4 (de Skolem) Sea A una formula cerrada en L1 = L1(C,F ,P ).
Entonces existen dos conjuntos finitos csk y fsk y una formula en forma nor-
mal de Skolem B en Lsk1 = L1(C ∪ csk,F ∪ fsk,P ) tal que A y B son equi-
satisfacibles, es decir: A es satisfacible en L1 si y solo si B es satisfacible
en Lsk1 .
Podremos trabajar con formulas equisatisfacibles si estamos interesados
en estudiar la satisfacibilidad de un conjunto de formulas y, en particular, si
estudiamos la validez de una inferencia usando el principio de refutacion.
Los elementos del conjunto csk en el teorema anterior se denominan cons-
tantes de Skolem y los elementos de fsk se denominan funciones de Skolem.
El proceso por el que determinamos estos conjuntos y la formula B a partir
de A se denomina skolemizacion.
Skolemizacion. Sea A una formula en forma normal prenexa y x1, . . . , xn
las variables que aparecen cuantificadas existencialmente en el prefijo de A
y en ese orden, leıdas de izquierda a derecha. Construimos una secuencia
de formulas A0, A1, . . . , An, y dos secuencias de conjuntos csk0, . . . , cskn,
fsk0, . . . , fskn, tales que: A0 = A, csk0 = ∅, fsk0 = ∅; An = B esta en
forma normal de Skolem; cada Ai es equisatisfacible a A; la formula Ai+1 se
obtiene a partir de Ai como sigue:
1. Si Ai = ∃xi+1Mi, consideramos a 6∈ C ∪ cski y tomamos:
cski+1 = cski ∪ a, fski+1 = fski, Ai+1 = [xi/a]Mi.
2. Si Ai = ∀y1 . . . ∀ym∃xi+1Mi, consideramos f 6∈ C ∪ fski y tomamos:
cski+1 = cski, fski+1 = fski ∪ f,
Ai+1 = ∀y1 . . . ∀ym[xi/f(y1, . . . , ym)]Mi.
En adelante, y en particular en el ejemplo siguiente, usaremos el sımbolo
≈ para representar la relacion de equisatisfacibilidad.
Ejemplo 5.1.3
A = A0 = ∃x∀y∃zP (x, y, z) ≈ A1 = ∀y∃zP (a, y, z) ≈ A2 = ∀yP (a, y, f(y))
I. T. en Informatica de Sistemas
4 Logica Computacional
Para este ejemplo, csk = a y fsk = f.
A = A0 = ∀x∀y∃z(P (f(x)) → R(y, z)) ≈ A1 = ∀x∀y(P (f(x)) → R(y, g(x, y)))
Para este ejemplo, csk = ∅ y fsk = g.
5.1.2. Interpretaciones de Herbrand
Definicion 5.5 Sea S una conjunto finito de formulas en forma normal de
Skolem en el lenguaje L1(CS ,F S ,P S) tal que la signatura contiene unica-
mente los sımbolos que aparecen en S, excepto si S no contiene sımbolos de
constante, en cuyo caso CS = a.
1. Llamamos Universo de Herbrand de S, y lo denotamos por HS, al con-
junto de terminos basicos construidos sobre los sımbolos del lenguaje, es
decir,
HS = T B(CS ,F S)
2. Llamamos Base de Herbrand de S, y lo denotamos BS al conjunto de
atomos basicos que se pueden construir sobre el Universo de Herbrand,
es decir,
BS = Atom(CS ,F S ,P S)
3. Llamamos Interpretacion de Herbrand para S a cualquier interpretacion
sobre el Universo de Herbrand, es decir, a las interpretaciones
I : Atom(CS ,F S ,P S) → 0, 1
Para evitar que el universo sea vacıo, hemos considerado CS = a en el
caso en que S no contenga constantes; a la constante a, que no aparece en S,
se la suele llamar constante de Herbrand.
Para el estudio de la satisfacibilidad de formas normales de Skolem es sufi-
ciente trabajar con interpretaciones de Herbrand. Por lo tanto, por el principio
de refutacion y la existencia de formas normales de Skolem equisatisfacibles,
podemos restringirnos a interpretaciones de Herbrand para el estudio de la
validez.
Teorema 5.6 (de Herbrand) Si S es un conjunto de formulas cerradas y
en forma normal de Skolem, entonces S es satisfacible si y solo si tiene un
modelo de Herbrand.
E.T.S.I.Informatica
Tema 5: Resolucion. 5
Optimizacion de la forma normal prenexa. El tamano del Universo de
Herbrand y por lo tanto la complejidad del conjunto de interpretaciones de
Herbrand, depende del conjunto de constantes y funciones de Skolem generado
durante la skolemizacion; a su vez, el tamano de estos conjuntos depende de
la formula en forma normal prenexa de la que partimos. Como hemos visto
en los ejemplos 5.1.1 y 5.1.2, en algunos casos podremos optar por aplicar las
equivalencias en distintos ordenes y obtener diferentes prefijos. Con el objetivo
de reducir la complejidad del Universo de Herbrand, es conveniente seguir las
siguiente reglas en el proceso de obtencion de la forma normal prenexa.
Cuando sea posible elegir, se extraeran en primer lugar aquellos cuanti-
ficadores que queden en el prefijo como existenciales.
Para reducir la longitud del prefijo, siempre que sea posible, renombra-
remos las variables para poder utilizar las equivalencias
∀xA ∧ ∀xB ≡ ∀x(A ∧ B),
∃xA ∨ ∃xB ≡ ∃x(A ∨ B),
∀xA → ∃xB ≡ ∃x(A → B).
5.1.3. Algoritmo de Gilmore
La conclusion practica inmediata que se obtiene una vez presentada la
semantica de Herbrand, es la posibilidad de trabajar en la logica de primer
orden de la misma forma que trabajamos en la logica proposicional. Podrıamos
construir tablas de verdad de las formulas, en donde las variables proposicio-
nales son sustituidas por elementos de la Base de Herbrand. Naturalmente, en
este caso es posible que estas tablas de verdad sean infinitas y, por lo tanto,
no podemos considerarlas como un metodo de demostracion adecuado. Sin
embargo, si permiten entender otros metodos de demostracion.
El metodo mas simple que se puede definir es la generalizacion del metodo
de Quine, y que en este caso se denomina Algoritmo de Gilmore. Su funcio-
namiento es identico al de Quine considerando los elementos de la base de
Herbrand para definir las evaluaciones parciales de las formulas.
Ejemplo 5.1.4 Vamos a estudiar la validez de una inferencia utilizando el
principio de refutacion y el algoritmo de Gilmore sobre la base de Herbrand
de la formula obtenida tras hallar una formula en forma normal de Skolem a
partir de la refutacion:
∀x(∃xP (x) → Q(x)) |= ∀y∀x(P (x) → Q(y))
⇔ ∀x(∃xP (x) → Q(x)),¬∀y∀x(P (x) → Q(y)) es insatisficible,
I. T. en Informatica de Sistemas
6 Logica Computacional
⇔ ∀x∀y(P (y) → Q(x)),∃y∃x¬(P (x) → Q(y)) es insatisficible,
⇔ ∀x∀y(P (y) → Q(x)),¬(P (b) → Q(a)) es insatisficible,
⇔ S = ∀x∀y(P (y) → Q(x)) ∧ ¬(P (b) → Q(a)) es insatisficible.
Dado que S no contiene funciones, el universo de Herbrand esta formado
simplemente por las constantes, HS = a, b, y la base de herbrand es fi-
nita, BS = P (a), Q(a), P (b), Q(b). Llamemos A1 = ∀x∀y(P (y) → Q(x))
y A2 = ¬(P (b) → Q(a)). Para entender mejor el arbol que construimos a
continuacion, es conveniente observar que los modelos de Herbrand de A1 =
∀x∀y(P (y) → Q(x)) coinciden con los de la formula
(P (a) → Q(a)) ∧ (P (a) → Q(b)) ∧ (P (b) → Q(a)) ∧ (P (b) → Q(b));
las dos formulas no son logicamente equivalentes, pero sı son equivalentes en
el universo de Herbrand.
P (b) ¬P (b)
0 (Por A2)
Q(a)
0 (Por A2)
¬Q(a)
0 (x = a, y = b en A1)
Ejemplo 5.1.5 Aunque el universo de Herbrand sea infinito, si la inferencia
es valida, siempre podremos encontrar un arbol finito que lo demuestre.
∀xP (x),∀x(P (x) → Q(f(x))) |= Q(f(a)) ⇔
⇔ S = ∀xP (x) ∧ ∀x(P (x) → Q(f(x))) ∧ ¬Q(f(a)) es insatisfacible
El universo de Herbrand es
HS = a, f(a), f(f(a), f(f(f(a))), . . .
y la base de Herbrand es
BS = P (a), Q(a), P (f(a)), Q(f(a)), P (f(f(a))), Q(f(f(a))), . . . .
Llamemos A1 = ∀xP (x), A2 = ∀x(P (x) → Q(f(x))) y A3 = ¬Q(f(a)) para
construir el arbol de Gilmore.
E.T.S.I.Informatica
Tema 5: Resolucion. 7
P (a) ¬P (a)
0 (x = a en A1)
Q(f(a))
0 (Por A3)
¬Q(f(a))
0 (x = a en A2)
Ejemplo 5.1.6 El razonamiento
∃x(P (x) ∧ ∀y(D(y) → L(x, y)))
∀x(P (x) → ∀y(Q(y) → ¬L(x, y)))
∀x(D(x) → ¬Q(x))
es valido si y solo si el siguiente conjunto es insatisfacible:
∃x(P (x) ∧ ∀y(D(y) → L(x, y))),
∀x(P (x) → ∀y(Q(y) → ¬L(x, y))),
¬∀x(D(x) → ¬Q(x))
Este conjunto es insatisfable si y solo si lo es el siguiente conjunto de formulas
en forma normal prenexa:
∃x∀y(P (x) ∧ (D(y) → L(x, y))),
∀x∀y(P (x) → (Q(y) → ¬L(x, y))),
∃x¬(D(x) → ¬Q(x))
Y este es insatisfacible si y solo si lo es el siguiente conjunto formado por
formulas en forma normal de Skolem:
∀y(P (a) ∧ (D(y) → L(a, y))),
∀x∀y(P (x) → (Q(y) → ¬L(x, y))),
¬(D(b) → ¬Q(b))
El universo de Herbrand es HS = a, b y la base de Herbrand
BS = P (a), P (b), Q(a), Q(b),D(a),D(b), L(a, a), L(a, b), L(b, a), L(b, b)
Construimos el arbol de Gilmore para A1 ∧ A2 ∧ A3, en donde
A1 = ∀y(P (a) ∧ (D(y) → L(a, y))),
A2 = ∀x∀y(P (x) → (Q(y) → ¬L(x, y))),
A3 = ¬(D(b) → ¬Q(b)).
I. T. en Informatica de Sistemas
8 Logica Computacional
D(b) ¬D(b)
0 (por A3)
Q(b) ¬Q(b)
0 (por A3)
P (a) ¬P (a)
0 (por A1)
L(a, b) ¬L(a, b)
0 (x = a, y = b en A2))0 (y = b en A1))
Ejemplo 5.1.7 Vamos a estudiar la validez del siguiente razonamiento usan-
do el metodo de Gilmore y el de las Tablas semanticas.
El padre del padre de una persona es su abuelo, toda persona tiene
un padre; por lo tanto todo el mundo tiene un abuelo.
Leyendo la relacion P (x, y) como “x es padre de y” y la relacion A(x, y) como
“x es abuelo de y” podemos escribir la siguiente formalizacion:
∀x∀y∀z((P (x, y) ∧ P (y, z)) → A(x, z))
∀x∃yP (y, x)
∀x∃yA(y, x)
Este razonamiento es valido si y solo si el siguiente conjunto es satisfacible:
∀x∀y∀z((P (x, y) ∧ P (y, z)) → A(x, z)),∀xP (f(x), x),∀y¬A(y, a)
Su dominio de Herbrand es
HS = a, f(a), f(f(a)), f(f(f(a))), . . .
y la base de Herbrand
BS = P (t1, t2); t1, t2 ∈ HS ∪ A(t1, t2); t1, t2 ∈ HS
Construimos el arbol de Gilmore para A1 ∧ A2 ∧ A3 con:
A1 =∀x∀y∀z((P (x, y) ∧ P (y, z)) → A(x, z)),
A2 =∀xP (f(x), x), A3 =∀y¬A(y, a)
E.T.S.I.Informatica
Tema 5: Resolucion. 9
P (f(a), a) ¬P (f(a), a)
0 (x = a en A2)
P (f(f(a)), f(a)) ¬P (f(f(a)), f(a))
0 (x = f(a) en A2)
A(f(f(a)), a) ¬A(f(f(a)), a)
0 (y = f(f(a)) en A3))0 (x = f(f(a)), y = f(a), z = a en A1))
La tabla semantica que demuestra igualmente la validez del razonamiento
se muestra a continuacion. La diferencia de tamano entre los dos arboles no
debe conducir a conclusiones erroneas sobre la complejidad de los metodos.
Debe tenerse en cuenta que, por una parte, el metodo de Gilmore requiere un
proceso de normalizacion previo y que, ademas, en ambos casos hemos elegido
un orden optimo para las sucesivas extensiones de los arboles.
∀x∀y∀z((P (x, y) ∧ P (y, z)) → A(x, z)) (7):c
∀x∃yP (y, x) (2):a (4):b
¬∀x∃yA(y, x) 4(1):a
¬∃yA(y, a) (6):c
∃yP (y, a) 4(3):b
P (b, a)
∃yP (y, b) 4(5)
P (c, b)
¬A(c, a)
∀y∀z((P (c, y) ∧ P (y, z)) → A(c, z)) (8):b
∀z((P (c, b) ∧ P (b, z)) → A(c, z)) (9):a
(P (c, b) ∧ P (b, a)) → A(c, a) 4(10)
¬(P (c, b) ∧ P (b, a)) 4(11) A(c, a)
8
¬P (c, b) ¬P (b, a)
8 8
Es interesante comparar las dos soluciones. En las dos, hemos necesitado tres
elementos para lograr las inconsistencias: a, b y c en las tablas y a, f(a) y
f(f(a)) en el arbol de Gilmore. Ademas, en ambos casos, el significado de los
mismos en el modelo es el mismo: b es el padre de a y c es el padre de b,
ası como f(a) es el padre de a y f(f(a)) es el padre de f(a).
I. T. en Informatica de Sistemas
10 Logica Computacional
5.2. Resolucion en la L. C. Proposicional
5.2.1. Forma clausal
Definicion 5.7 Decimos que una formula de la Logica Clasica Proposicional
esta en forma normal conjuntiva si es ⊥, ⊤ o una conjuncion de clausulas.
Decimos que esta en forma normal conjuntiva restringida si las clausulas y
cubos que contiene son restringidos y no contiene una clausula que subsuma a
otra.
En el tema 3 demostramos que cualquier formula es equivalente a una
formula en forma normal negativa. A partir de esta y usando la distributividad
de la disyuncion respecto de la conjuncion, conseguimos una formula en forma
normal conjuntiva. Finalmente, aplicando las siguientes equivalencias tantas
veces como sea posible, obtenemos la forma restringida:
A ∧ A ≡ A, ¬A ∧ A ≡ ⊥, ⊤ ∧ A ≡ A, ⊥ ∧ A ≡ ⊥,
A ∨ A ≡ A, ¬A ∨ A ≡ ⊤, ⊥ ∨ A ≡ A, ⊤ ∨ A ≡ ⊤,
A ∨ (A ∧ B) ≡ A A ∧ (A ∨ B) ≡ A.
Obtenemos ası es siguiente resultado.
Teorema 5.8 Si A es una formula de la Logica Clasica Proposicianal, es
posible construir una formula C en forma normal conjuntiva restringida tal
que A ≡ C.
Dado que estamos interesados en trabajar con el principio de refutacion, pode-
mos utilizar propiedades de equisatisfacibilidad. En particular, sabemos que la
satisfacibilidad de un conjunto de formulas es equivalente a la satisfacibilidad
de su conjuncion; esto nos permite establecer el siguiente corolario.
Corolario 5.9 Si Ω es un conjunto de formulas de la Logica Clasica Propo-
sicianal, es posible construir un conjunto de clausulas restringidas Γ tal que Ω
es satisfacible si y solo si Γ es satisfacible. Decimos que Γ es la forma clausal
de Ω.
Ejemplo 5.2.1 Para estudiar la validez del razonamiento
A1 p → (q ∨ r)
A2 (q ∧ s) → p
A3 r → p
C s → (p ↔ (q ∨ r))
E.T.S.I.Informatica
Tema 5: Resolucion. 11
obtenemos la forma clausal del conjunto que se obtiene tras refutar la conclu-
sion:
A1 = p → (q ∨ r) ≡ ¬p ∨ q ∨ r
A2 = (q ∧ s) → p ≡ ¬q ∨ ¬s ∨ p
A3 = r → p ≡ ¬r ∨ p
¬C ≡ s ∧ (p ∨ q ∨ r) ∧ (¬q ∨ ¬p) ∧ (¬r ∨ ¬p)
Los detalles de la conversion en forma normal conjuntiva restringida de ¬C
son los siguientes:
¬C = ¬(s → (p ↔ (q ∨ r)))
≡ ¬(¬s ∨ ((¬p ∨ q ∨ r) ∧ (p ∨ ¬(q ∨ r))))
≡ s ∧ ((p ∧ ¬q ∧ ¬r) ∨ (¬p ∧ (q ∨ r)))
≡ s ∧ (p ∨ ¬p) ∧ (p ∨ q ∨ r) ∧ (¬q ∨ ¬p) ∧
∧ (¬q ∨ q ∨ r) ∧ (¬r ∨ ¬p) ∧ (¬r ∨ q ∨ r)
≡ s ∧ (p ∨ q ∨ r) ∧ (¬q ∨ ¬p) ∧ (¬r ∨ ¬p)
Por lo tanto, la forma clausal de A1, A2, A3,¬C es
Γ = ¬p ∨ q ∨ r,¬q ∨ ¬s ∨ p,¬r ∨ p, s, p ∨ q ∨ r,¬q ∨ ¬p,¬r ∨ ¬p
5.2.2. Resolucion como Sistema de Demostracion
El metodo de Resolucion que vamos a estudiar en este tema se define sobre
un lenguaje muy reducido, el de las clausulas restringidas.
Alfabeto: Q ∪ ¬,∨,⊤,2,
Gramatica: Las formulas bien formadas son ⊤, 2 y las clausulas restringidas.
En este contexto, usamos el sımbolo 2 en lugar de ⊥ para representar la
insatisfacibilidad; ademas, esta formula se denomina clausula vacıa. La teorıa
mostrada en la seccion anterior demuestra que el lenguaje de las clausulas es
suficiente para caracterizar la validez en la Logica Clasica.
Definicion 5.10 En el lenguaje de clausulas restringidas definimos las si-
guiente operaciones.
I. T. en Informatica de Sistemas
12 Logica Computacional
1. Si C es una clausula restringida y ℓ es un literal de C:
Crℓ :=
2 si C = ℓ
ℓ1 ∨ · · · ∨ ℓk−1 ∨ ℓk · · · ∨ ℓn si C = ℓ1 ∨ · · · ∨ ℓk−1 ∨ ℓ ∨ ℓk · · · ∨ ℓn
2. Si el literal ℓ pertenece a la clausula C1 y ℓ pertenece a C2, decimos que
C1 y C2 son resolubles respecto a ℓ y llamamos resolvente de C1 y C2
respecto de ℓ a la clausula Rℓ(C1, C2) que resulta de obtener la forma
restringida de
(C1rℓ) ∨ (C2rℓ)
Ejemplo 5.2.1
C = ¬p ∨ q ∨ ¬r; Cr¬p = q ∨ ¬r
C = ¬p ∨ q ∨ ¬r; Crr = C
C = q; Crq = 2(= ⊥)
R¬p(¬p ∨ q ∨ ¬r, q ∨ p ∨ t) = q ∨ ¬r ∨ t
Rp(p,¬p) = 2
C1 = q ∨ ¬r, C2 = p ∨ ¬r no son resolubles respecto de ningun literal.
Rp(q ∨ r,¬r ∨ p) NO existe.
El Sistema por Resolucion se describe con una unica regla de inferencia,
la Regla de Resolucion.
Definicion 5.11
1. Regla de resolucion: Si C1 y C2 son resolubles respecto a ℓ, entonces:
Rℓ(C1, C2) es consecuencia inmediata de C1 y C2.
2. Dado un conjunto de clausulas restringidas Ω, decimos que C es dedu-
cible por resolucion a partir de Ω, y lo denotamos Ω ⊢R C, si existe una
secuencia finita y ordenada de clausulas C1, . . . , Cn tal que Cn = C y
cada clausula es o bien un elemento de Ω o bien consecuencia inmediata
de las anteriores por la regla de resolucion. La secuencia de clausulas
se denomina deduccion por Resolucion de C desde Ω; y si C = 2 la
secuencia se denomina simplemente refutacion por resolucion.
Ejemplo 5.2.2 2 es deducible por resolucion a partir de
Ω = p ∨ q,¬q ∨ r,¬p ∨ r,¬r :
E.T.S.I.Informatica
Tema 5: Resolucion. 13
1. ¬p ∨ r ∈ Ω
2. ¬r ∈ Ω
3. ¬p = Rr(1, 2)
4. ¬q ∨ r ∈ Ω
5. ¬q = R¬r(2, 4)
6. p ∨ q ∈ Ω
7. q = R¬p(3, 6)
8. 2 = R¬q(5, 7)
Segun vemos a continuacion, al encontrar una deduccion por resolucion para
Ω, podemos deducir que este conjunto es insatisfacible.
Teorema 5.12 Un conjunto de clausulas restringidas es insatisfacible si y
solo si es posible construir una refutacion por resolucion. Es decir,
Ω |= ⊥ si y solo si Ω ⊢R 2
Este teorema garantiza la correccion y completitud de la regla de resolucion
gracias a la existencia de formas clausales equisatisfacibles.
Ejemplo 5.2.3 En el ejemplo 5.2.1 hemos visto que el razonamiento
A1 p → (q ∨ r)
A2 (q ∧ s) → p
A3 r → p
C s → (p ↔ (q ∨ r))
es valido si y solo si el conjunto
Γ = ¬p ∨ q ∨ r,¬q ∨ ¬s ∨ p,¬r ∨ p, s, p ∨ q ∨ r,¬q ∨ ¬p,¬r ∨ ¬p
es insatisfacible. Una refutacion por resolucion que lo prueba es la siguiente:
1. ¬p ∨ q ∨ r
2. ¬q ∨ ¬s ∨ p
3. ¬r ∨ p
4. s
5. p ∨ q ∨ r
6. ¬q ∨ ¬p
I. T. en Informatica de Sistemas
14 Logica Computacional
7. ¬r ∨ ¬p
8. ¬q ∨ p R(2,4)
9. p ∨ r R(8,5)
10. p R(3,9)
11. ¬q R(6,10)
12. ¬p ∨ r R(1,11)
13. r R(9,12)
14. ¬r R(7,10)
15. 2 R(13,14)
5.2.3. Resolucion como algoritmo
Si el conjunto de clausulas cuya satisfacibilidad estamos estudiando es
finito, el conjunto de las variables proposicionales tambien es finito y por lo
tanto, tambien es finito el conjunto de resolventes que podemos obtener, ya
que estas deben ser clausulas restringidas. En consecuencia, es posible generar
todas las resolventes, lo que nos lleva al algoritmo basico construible sobre la
regla de resolucion: generar sistematicamente todas las resolventes a partir de
un conjunto de clausulas dado; si este conjunto contiene la clausula vacıa, el
conjunto es insatisfacible, en caso contrario, es satisfacible.
Ejemplo 5.2.4 Para estudiar la satisfacibilidad de
Ω = p ∨ q, p ∨ r,¬q ∨ ¬r,¬p
vamos a generar sistematicamente todas las posibles resolventes, comprobando
si cada clausula es resoluble con “todas” las demas y comprobando si cada
nueva resolvente es a su vez resoluble con todas las demas.
1. p ∨ q
2. p ∨ r
3. ¬q ∨ ¬r
4. ¬p
5. p ∨ ¬r R(1, 3)
6. q R(1, 4)
7. p ∨ ¬q R(2, 3)
8. r R(2, 4)
E.T.S.I.Informatica
Tema 5: Resolucion. 15
9. p R(1, 7)
10. ¬r R(3, 6)
11. ¬q R(3, 8)
12. 2 R(4, 9)
Paramos en cuanto generamos la clausula vacıa en la lınea 12. Por otra parte,
dado que estamos construyendo un conjunto, las resolvente que ya hayamos
generado anteriormente, no las anotamos.
Los refinamientos del metodo basico de resolucion consisten en reducir el
tamano del conjunto de posibles resolventes que debemos generar para buscar
la clausula vacıa o concluir que no es posible hacerlo. En la ultima parte
del tema estudiaremos dos refinamientos que aplicaremos simultaneamente:
resolucion lineal y resolucion ordenada.
5.3. Resolucion en la L. C. de P. de Primer Orden
5.3.1. Forma clausal
Definicion 5.13 Decimos que una formula de la Logica Clasica Predicados
de Primer Orden esta en forma normal prenexa conjuntiva si esta en forma
normal prenexa y su matriz esta en forma normal conjuntiva.
Para definir la forma clausal en la logica de Primer Orden, debemos en
primer lugar establecer la nocion de clausula: llamamos clausula al cierre uni-
versal de una disyuncion de literales. Por ejemplo:
∀x∀y(¬P (x, a) ∨ Q(a, f(y))
es una clausula, pero ∃x(P (x) ∨ Q(x)) no lo es, puesto que el prefijo contiene
un cuantificador existencial.
Si una formula esta en forma normal prenexa conjuntiva y ademas el pre-
fijo no contiene cuantificadores existenciales, entonces es posible escribir esa
formula como una conjuncion de clausulas haciendo uso de la equivalencia
∀x(A(x) ∧ B(x)) ≡ ∀xA(x) ∧ ∀xB(x) (5.4)
Por lo tanto, el proceso de obtencion de la forma normal de Skolem, la distri-
butividad para obtener la forma normal conjuntiva, la equivalencia (5.4) y la
eliminacion de conjunciones permiten establecer el siguiente resultado
I. T. en Informatica de Sistemas
16 Logica Computacional
Teorema 5.14 Dado un conjunto Ω de formulas de la Logica Clasica de Pre-
dicados de Primer Orden, es posible construir un conjunto Γ de clausulas tal
que Γ es satisfacible si y solo si Ω es satisfacible. Decimos que el conjunto Γ
es la forma clausal de Ω.
Ejemplo 5.3.1 En este ejemplo, mostramos los distintos pasos que conducen
a la obtencion de la forma clausal de la refutacion de un razonamiento.
∀x((P (x) → Q(x)) ∧ (Q(x) → R(x))) |= ∀x(P (x) → R(x)),
⇔ ∀x((P (x) → Q(x)) ∧ (Q(x) → R(x)),¬∀x(P (x) → R(x)) es insatisfa-
cible,
⇔ ∀x((¬P (x)∨Q(x))∧(¬Q(x)∨R(x)),∃x(P (x)∧¬R(x)) es insatisfacible,
⇔ ∀x((¬P (x) ∨ Q(x) ∧ (¬Q(x) ∨ R(x)), P (a) ∧ ¬R(a) es insatisfacible,
⇔ ∀x(¬P (x) ∨ Q(x)),∀x(¬Q(x) ∨ R(x)), P (a),¬R(a) es insatisfacible.
El orden en el que se aplican los distintos pasos puede alterarse excepto el de
skolemizacion, que debe ser siempre posterior al de refutacion y aplicarse a
formulas en forma prenexa.
Para abreviar, es frecuente omitir el prefijo en las clausulas. Ası, en el
ejemplo anterior escribiremos simplemente
¬P (x) ∨ Q(x),¬Q(x) ∨ R(x), P (a),¬R(a).
Debemos tener cuidado con esta simplificacion y entender que, aunque no se
muestren explıcitamente, las clausulas estan cuantificadas universalmente y,
lo que es mas importante, que estan independientemente cuantificadas. Por
ejemplo, siguiendo con el ejemplo anterior, determinar una instancia de la
primera clausula, ¬P (x) ∨ Q(x), no obliga realizar la misma operacion en la
segunda, ¬Q(x) ∨ R(x), aunque la variable sea la misma. Esto es ası porque
las dos variables ‘x’ estan ligadas por distintos cuantificadores y al liberar una
de ellas para instanciarla, no liberamos a la otra.
La regla de resolucion se basa en enfrentar dos literales opuestos en dos
clausulas. Dado que las clausulas en la logica de Primer Orden estan universale-
mente cuantificadas, debemos entender que representan a todas sus instancias
en el universo de Herbrand. De esta forma, una resolvente de dos clausulas se
obtendrıa al enfrentar instancias de dos clausulas.
E.T.S.I.Informatica
Tema 5: Resolucion. 17
Ejemplo 5.3.2 La validez del razonamiento
∀x((E(x) ∧ ¬V (x)) → ∃y(S(x, y) ∧ C(y)))
∃x(P (x) ∧ E(x) ∧ ∀y(S(x, y) → P (y)))
∀x(P (x) → ¬V (x))
∃x(P (x) ∧ C(x))
es equivalente a la insatisfacibilidad del conjunto
∀x(¬E(x) ∨ V (x) ∨ S(x, f(x))), ∀x(¬E(x) ∨ V (x) ∨ C(f(x))),
∀x(¬S(a, y) ∨ P (y)), ∀x(¬P (x) ∨ ¬V (x)),
∀x(¬P (x) ∨ ¬C(x)), P (a), E(a)
El Universo de Herbrand de este conjunto de clausulas es
H = a, f(a), f(f(a)), f(f(f(a))), . . .
y, por lo tanto, los modelos de Herbrand son los modelos de Herbrand del
conjunto:
Γ = P (a), E(a) ∪⋃
t∈H
¬E(t) ∨ V (t) ∨ S(t, f(t)),¬E(t) ∨ V (t) ∨ C(f(t)),
¬S(a, t) ∨ P (t),¬P (t) ∨ ¬V (t),¬P (t) ∨ ¬C(t)
El conjunto Γ no tiene cuantificadores y por lo tanto, su satisfacibilidad puede
estudiarse usando el metodo de resolucion para la logica proposicional.
1. P (a) ∈ Γ
2. ¬P (a) ∨ ¬V (a) ∈ Γ
3. ¬V (a) R(1,2)
4. ¬E(a) ∨ V (a) ∨ C(f(a)) ∈ Γ
5. E(a) ∈ Γ
6. V (a) ∨ C(f(a) R(4,5)
7. C(f(a)) R(3,6)
8. ¬E(a) ∨ V (a) ∨ S(a, f(a)) ∈ Γ
9. V (a) ∨ S(a, f(a)) R(5,8)
10. S(a, f(a)) R(9,3)
11. ¬S(a, f(a)) ∨ P (f(a)) ∈ Γ
12. P (f(a)) R(10,11)
13. ¬P (f(a)) ∨ ¬C(f(a)) ∈ Γ
14. ¬C(f(a)) R(12,13)
15. 2 R(13,14)
I. T. en Informatica de Sistemas
18 Logica Computacional
5.3.2. Unificacion
El metodo seguido en el ejemplo anterior consiste en elegir entre las ins-
tancias basicas para buscar las resolventes siguiendo el sistema de la logica
proposicional. Debemos entender que este es el metodo fundamental en el que
se basa la resolucion en la logica de primer orden; muchas dudas y proble-
mas que nos surjan en la aplicacion de los refinamientos posteriores pueden
resolverse facilmente analizandolos desde el punto de vista de este metodo
basico.
El refinamiento fundamental que aplicamos en primer lugar consiste en
trabajar con instancias, no necesariamente basicas, que representen varias re-
solventes. Por ejemplo, todas las instancias basicas de la clausula
∀y(A(f(y)) ∨ B(f(y)))
son resolventes de las clausulas
∀x(A(x) ∨ ¬P (x)) y ∀y(B(y) ∨ P (f(y)))
ya que todas las instancias de ∀y(A(f(y)) ∨ ¬P (f(y))) tambien los son de
∀x(A(x) ∨ ¬P (x)). Para obtener estas resolventes, de la manera mas general
posible, necesitamos utilizar el algoritmo de unificacion.
Definicion 5.15 Una sustitucion σ : L1 → L1 es un unificador para las
formulas atomicas A y B si σA = σB. Decimos que σ es el unificador mas
general si dado otro unificador θ, existe una sustitucion λ tal que θ = λ σ.
Teorema 5.16 El algoritmo que se describe a continuacion, determina si dos
formulas atomicas A y B son o no unificables y en su caso, determina el
unificador mas general.
Algoritmo de unificacion. Dadas dos formulas atomicas A y B con el
mismo sımbolo de predicado, el siguiente algoritmo determina en cada paso
una sustitucion σi = [xi/ti] o concluye que las dos formulas no son unificables.
Si son unificables, el algoritmo concluye con la construccion de una secuencia
finita de sustituciones σ1 = [x1/t1],. . . ,σn = [xn/tn] de tal forma que
σn . . . σ1A = σn . . . σ1B.
Consideramos A0 = A, σ0 = Id (aplicacion identidad); si Am−1 = σm−1 . . . σ1A
y Bm−1 = σm−1 . . . σ1B, entonces:
E.T.S.I.Informatica
Tema 5: Resolucion. 19
1. Si Am−1 = Bm−1, el algoritmo finaliza: las formulas son unificables y el
unificador mas general es σm−1 . . . σ1.
2. Si Am−1 6= Bm−1, recorremos los sımbolos de Am−1 y Bm−1 de izquierda
a derecha y localizamos el primero de cada formula en que difieren y
consideramos los terminos mas pequenos que contienen a estos sımbolos:
a) Si ninguno de estos dos terminos es una variable, el algoritmo fina-
liza: A y B no son unificables.
b) Si uno de los dos terminos es una variable y esta aparece en el otro
termino, el algoritmo finaliza: A y B no son unificables.
c) Si x es uno de los terminos y t es el otro (x no pertenece a t),
consideremos σm = [x/t] y volvemos al incio del algoritmo.
Ejemplo 5.3.1
P (x, a) y Q(y) no son unificables, ya que no tienen el mismo sımbolo de
predicado.
P (x, a) y P (x, f(x, y)) no son unificables. Los terminos subrayados son
los que distinguen a las formulas; dado que a es una constante y f(x, y)
es un termino con funcion f , el paso 2.a del algoritmo concluye que las
formulas no son unificables.
P (x, f(g(y), z)) y P (x, f(y, z)) no son unificables, ya que la variable y
aparece en el termino f(y) (paso 2.b del algoritmo).
P (a, x, f(g(y))) y P (z, f(z), f(u)) son unificables:
4 A0 = P (a, x, f(g(y))) y B0 = P (z, f(z), f(u)):
por el paso 2.c del algoritmo, tomamos σ1 = [z/a].
4 A1 = P (a, x, f(g(y))) y B1 = P (a, f(a), f(u)):
por el paso 2.c del algoritmo, tomamos σ2 = [x/f(a)].
4 A2 = P (a, f(a), f(g(y))) y B2 = P (a, f(a), f(u)):
por el paso 2.c del algoritmo, tomamos σ3 = [u/g(y)].
4 A3 = P (a, f(a), f(g(y))) = B3 y por lo tanto, concluimos que las
formulas iniciales son unificables y que el unificador mas general es
σ3 σ2 σ1 = [u/g(y)] [x/f(a)] [z/a]
5.3.3. Resolucion en la L. C. de Primer Orden
Ya tenemos las herramientas necesarias para definir la regla de resolucion
en la Logica Clasica de Primer Orden sobre clausulas con variables.
I. T. en Informatica de Sistemas
20 Logica Computacional
Definicion 5.17
Sean C1 y C2 dos clausulas que no comparten variables y sean ℓ1 y ℓ2
dos literales en C1 y C2 respectivamente tales que ℓ1 y ℓ2 son unificables
y σ es su unificador mas general; entonces C1 y C2 son resolubles y la
forma restringida de clausula
(σC1rσL1) ∨ (σC2rσL2)
se denomina resolvente binaria de C1 y C2 respecto de L1 y se denota
R(C1, C2).
(RB) Resolvente binaria: si C1 y C2 son resolubles, entonces
R(C1, C2) es consecuencia inmediata a partir C1 y C2.
Si dos literales con el mismo signo de un clausula C son unificables y su
unificador mas general es σ, entonces la forma restringida de la clausula
σC se denomina factor de C.
(FB) Factor binario: si C ′ es un factor de C, entonces C ′ es
consecuencia inmediata de C.
Dado un conjunto de clausulas restringidas Ω, decimos que C es dedu-
cible por resolucion a partir de Ω, y lo denotamos Ω ⊢R C, si existe una
secuencia finita y ordenada de clausulas C1, . . . , Cn tal que Cn = C y
cada clausula es o bien un elemento de Ω o bien consecuencia inmedia-
ta de las anteriores por las reglas (RB) o (FB) definidas en los puntos
anteriores. La secuencia de clausulas se denomina deduccion por Reso-
lucion de C desde Ω; si C = 2 la secuencia se denomina simplemente
refutacion por resolucion.
Ademas de la regla de resolucion, debemos considerar la posibilidad de
obtener factores. Estas clausulas se corresponden con las instancias basicas
del conjunto de clausulas en las que podemos eliminar literales repetidos; no
debemos olvidar que, tambien en la logica de primer orden, trabajamos con
clausulas restringidas.
Tambien debemos destacar la condicion impuesta sobre dos clausulas antes
de comprobar si son unificables: no pueden compartir variables. Recordemos
que cada clausula esta independientemente cuantificada y, por lo tanto, siem-
pre podemos renombrar las variables para conseguir esta condicion.
Teorema 5.18 Un conjunto de clausualas en la logica de primer orden es
insatisfacible si y solo si existe una refutacion por resolucion.
Ejemplo 5.3.3 Vamos a encontrar una refutacion por resolucion para el con-
junto
Ω = ¬F (x, a)∨¬F (x, t)∨¬F (t, x), F (x, a)∨F (x, f(x)), F (x, a)∨F (f(x), x)
E.T.S.I.Informatica
Tema 5: Resolucion. 21
1. ¬F (x, a) ∨ ¬F (x, t) ∨ ¬F (t, x) ∈ Ω
2. ¬F (x, a) ∨ ¬F (a, x) FB(1): σ = [t/a]
3. ¬F (a, a) FB(2): σ = [x/a]
4. F (x, a) ∨ F (x, f(x)) ∈ Ω
5. F (a, f(a)) RB(3, 4): σ = [x/a]
6. ¬F (f(a), a) RB(2, 5): σ = [x/f(a)]
7. F (x, a) ∨ F (f(x), x) ∈ Ω
8. F (a, a) RB(6, 7): σ = [x/a]
9. 2 RB(3, 8)
Ejemplo 5.3.4 Como ya hemos dicho, la regla (FB) es necesaria para ob-
tener un sistema deductivo completo. Consideremos el siguiente conjunto de
clausulas:
Ω = P (x) ∨ P (y),¬P (x) ∨ ¬P (y)
Salvo renombramientos de variables, la unica resolvente binaria que puede
obtenerse a partir de Ω es P (x)∨¬P (y), y por lo tanto, no podemos generar,
de esta forma, la clausula vacıa. Sin embargo, Ω es insatisfacible:
∀x∀y(P (x) ∨ P (y)) |= P (a)
∀x∀y(¬P (x) ∨ ¬P (y)) |= ¬P (a)
Ω |= P (a) ∧ ¬P (a) ≡ ⊥
5.4. Resolucion Lineal Ordenada
Como ya hemos dicho anteriormente, sobre el metodo basico de resolucion
en el que generamos todas las posibles resolventes hasta encontrar, si es posible,
la clausula vacıa, podemos establecer distintos refinamientos que reducen el
tamano del conjunto de resolventes en el que buscar la clausula vacıa. En esta
seccion vamos a estudiar dos refinamientos que aplicaremos simultaneamente:
Resolucion ordenada: las clausulas se consideran secuencias ordenadas
de literales y la eleccion del literal a resolver se eligen atendiendo a este
orden.
Resolucion lineal: en la secuencia de resolventes, siempre utilizamos la
ultima obtenida para hallar la siguiente.
I. T. en Informatica de Sistemas
22 Logica Computacional
Establecemos a continuacion, detalladamente, las definiciones necesarias
para describir el algoritmo del Resolucion Lineal Ordenada.
Consideramos las clausulas como secuencias ordenadas de literales, de tal
forma que dicho orden no puede ser alterado en el proceso de deduccion.
Para analizar si dos clausulas C1 y C2, son resolubles, solo miramos el
primer literal por la derecha de C1.
El literal resuelto en la clausula C1, se mantiene en la resolvente pero
marcado con un recuadro, excepto si este queda el primero por la derecha.
RO(¬q ∨ p,¬r ∨ ¬p ∨ ¬q) = ¬q ∨ p ∨ ¬r [= ¬q ∨ r]
RO(¬q ∨ p,¬p) = [¬q ∨ p ] = ¬q
RO(¬Q(x) ∨ P (x, a),¬R(z) ∨ ¬P (b, z) ∨ ¬Q(b)) =
= ¬Q(b) ∨ P (b, a) ∨ ¬R(a)
Las sustituciones que apliquemos posteriormente a estas resolventes ac-
tuaran igualmente sobre los literales recuadrados.
En caso de repeticion y al obtener factores, se elimina el literal repetido
de la derecha.
ROp(q ∨ p, r ∨ ¬p ∨ q) = [q ∨ p ∨ r ∨ q] = q ∨ p ∨ r
Sobre las clausulas con literales recuadrados, definimos la operacion de
Reduccion: si el primer literal por la derecha es unificable con el opuesto
de un literal recuadrado, aquel es eliminado:
Red(p ∨ ¬q ∨ ¬r ∨ q) = p ∨ ¬q ∨ ¬r = [RO(p ∨ ¬q, p ∨ ¬r ∨ q)]
Red(P (y) ∨ ¬Q(x, y) ∨ ¬R(x) ∨ Q(a, f(x)) =
= P (f(a)) ∨ ¬Q(a, f(a)) ∨ ¬R(a)
Los literales recuadrados guardan la informacion sobre clausulas que se han
obtenido previamente en el proceso de resolucion; la reduccion consiste en
obtener la resolvente entre la propia clausula y una de las clausulas recordada
por las marcas.
Algoritmo. El algoritmo de resolucion lineal ordenada consiste en la crea-
cion de uno o varios arboles en donde cada nodo y cada rama se etiquetan de
una de las siguientes formas:
C1
C2
RO(C1, C2)
C1
Factor(C1)
C1
Red(C1)
E.T.S.I.Informatica
Tema 5: Resolucion. 23
Las clausulas que etiquetan los nodos se denominan clausulas centrales y las
que etiqueta las ramas se denominan clausulas laterales.
1. La raız del primer arbol es cualquier clausula del conjunto Ω, C0 ∈ Ω;
esta clausula se denomina cabeza.
2. Cada rama del arbol se extiende anadiendo tantos hijos como clausulas
de Ω o factores de clausulas de Ω sean resolubles respecto al primer
literal por la derecha de la clausula de la hoja.
3. Si la clausula de una hoja es reducible, esta se extiende con una unica
rama cuyo nodo se etiqueta con la clausula reducida.
4. Una rama deja de extenderse si ocurre una de las siguientes situaciones:
La clausula de la hoja ya ha sido generada anteriormente en cual-
quier parte del arbol (y su rama se ha extendido o parado por otra
causa).
La clausula de la hoja es ⊤.
La clausula de la hoja no tiene factores y no es resoluble con ninguna
clausula de Ω.
5. Si detenemos todas las ramas sin generar 2, iniciamos la construccion
de otro arbol a partir del conjunto ΩrC0.
6. Si en cualquier arbol generamos la clausula vacıa, concluimos que el
conjunto es insatisfacible. Si todos los arboles son parados sin generar 2
concluimos que el conjunto es satisfacible.
Habitualmente, la extension de los arboles se hace buscando las ramas no
detenidas primero en profundidad. En el caso de primer orden, las implemen-
taciones de este algoritmo deben incluir varios mecanismos para evitar entrar
en “bucles”. En la aplicacion manual del algoritmo no consideraremos ninguno
de estos mecanismos, ya que pueden complicar en exceso su aplicacion. De la
misma forma, al aplicarlo manualmente es conveniente escribir cada rama de
manera independiente; si ella no nos lleva a la clausula vacıa, iniciaremos otra
rama del mismo arbol. Si trabajamos de esta forma, debemos estar seguros de
que hemos desarrollado todas las posibles ramas antes de eliminar la clausula
cabeza para iniciar un segundo arbol.
Ejemplo 5.4.1
Ω = p ∨ q,¬p ∨ ¬r,¬q ∨ ¬r,¬q ∨ ¬w, r ∨ w, q ∨ r
I. T. en Informatica de Sistemas
24 Logica Computacional
Ejemplo 5.4.2 Ω0 = ¬p∨¬q∨ r,¬q∨¬r∨¬s∨ p,¬r∨¬p∨ s,¬r∨¬s∨¬q
Iniciamos un segundo arbol para Ω1 = ¬q∨¬r∨¬s∨p,¬r∨¬p∨s,¬r∨¬s∨¬q
E.T.S.I.Informatica
Tema 5: Resolucion. 25
Dado que Ω2 = ¬r ∨ ¬p ∨ s,¬r ∨ ¬s ∨ ¬q esta formado por dos clausulas
que no son literales opuestos, podemos concluir que es satisfacible y en conse-
cuencia tambien lo es Ω.
Ejemplo 5.4.3 Ω = ¬R(x) ∨ ¬S(a),¬Q(x) ∨ R(x), Q(a) ∨ R(x), S(x) es
satisfacible
¬R(x) ∨ ¬S(a)
S(y)[y/a]
¬R(x)
Q(a) ∨ R(y)
[x/y]
¬R(y) ∨ Q(a)
¬Q(x) ∨ R(x)[x/a]
¬R(y) ∨ Q(a) ∨ R(a)
Reduccion, [y/a]
Ejemplo 5.4.4 Estudiemos la validez de A = ¬∃y∀x(F (x, y)↔¬∃z(F (x, z)∧
F (z, x))),
¬A = ∃y∀x(F (x, y) ↔¬∃z(F (x, z) ∧ F (z, x)))
≡ ∃y∀x((¬F (x, y) ∨ ¬∃z(F (x, z) ∧ F (z, x)))
∧ (F (x, y) ∨ ∃z(F (x, z) ∧ F (z, x))))
≡ ∃y∀x∃z((¬F (x, y) ∨ ∀t(¬F (x, t) ∨ ¬F (t, x)))
∧ (F (x, y) ∨ (F (x, z) ∧ F (z, x))))
≡ ∃y∀x∃z∀t((¬F (x, y) ∨ ¬F (x, t) ∨ ¬F (t, x))
∧ (F (x, y) ∨ F (x, z)) ∧ (F (x, y) ∨ F (z, x)))
≈ ∀x∀t((¬F (x, a) ∨ ¬F (x, t) ∨ ¬F (t, x))
∧ (F (x, a) ∨ F (x, f(x))) ∧ (F (x, a) ∨ F (f(x), x)))
Ω = ¬F (x, a)∨¬F (x, t)∨¬F (t, x), F (x, a)∨F (x, f(x)), F (x, a)∨F (f(x), x)
I. T. en Informatica de Sistemas
26 Logica Computacional
Factor, x/a, t/a: ¬F (a, a)
F (x, a) ∨ F (x, f(x))[x/a]
¬F (a, a) ∨ F (a, f(a))
¬F (x, a) ∨ ¬F (x, t) ∨ ¬F (t, x)Factor, [t/a]: ¬F (x, a) ∨ ¬F (a, x)[x/f(a)]
¬F (a, a) ∨ F (a, f(a)) ∨ ¬F (f(a), a)
F (x, a) ∨[x/a]
¬F (a, a) ∨ F (a, f(a)) ∨ ¬F (f(a), a) ∨ F (a, a)
Reduccion
¬F (x, a) ∨ ¬F (x, t) ∨ ¬F (t, x)
F (f(x), x)
5.5. Clausulas de Horn
Un programa logico es un conjunto de formulas que responden al siguiente
esquema
(A1 ∧ · · · ∧ An) → A
en donde A y cada Ai son atomos; en particular, no se incluye la negacion. Este
tipo de conjuntos responde a la idea de una base de conocimiento compuesta
por reglas. Si n = 0, la regla se reduce al atomo A; estas reglas se denominan
hechos. Cada atomo Ai debe ser distinto de ⊥, ya que en caso contrario la
regla serıa una tautologıa y por lo tanto superflua en el programa. El atomo A
sı puede ser ⊥; en ese caso, la regla es equivalente a la formula ¬(A1∧· · ·∧An)
y se denomina restriccion.
Si las reglas de un programa logico se convierten en forma clausal, obte-
nemos un conjunto de clausulas que contienen a los sumo un literal positivo.
Este tipo de clausulas se denominan clausulas de Horn y por lo tanto, trabajar
con programas logicos es equivalente a considerar conjuntos de clausulas de
Horn.
Siguiendo con la identificacion de los programas los logicos con bases de
conocimiento basadas en reglas, la realizacion de una consulta a esta base de
conocimiento se corresponde con el estudio de la validez de una inferencias.
Concretamente, hacer una consulta es preguntarse si una afirmacion A (atomo
del lenguaje) es deducible del programa, es decir, si la inferencia P |= A es
valida. Para estudiar la validez de esta inferencia usando resolucion, debemos
E.T.S.I.Informatica
Tema 5: Resolucion. 27
construir previamente la forma clausal de P ∪ ¬A que tambien estara for-
mada por clausulas de Horn.
La aplicacion del metodo de resolucion sobre conjuntos de clausulas de
Horn (y por lo tanto el estudio de consultas sobre un programa logico), admite
refinamiento mas fuertes, lo que recogemos en los siguientes resultados.
Lema 5.19 Sea Ω un conjunto de clausulas de Horn. Si todas las clausulas
contienen un literal positivo, entonces el conjunto es satisfacible.
Teorema 5.20 Sea Ω un conjunto de clausulas de Horn. Si Ω es insatisfaci-
ble, entonces existe una refutacion por resolucion lineal tal que:
La cabeza es una clausula negativa (no contiene literales positivos).
Las clausulas laterales son elementos de Ω.
Es decir, si aplicamos el algoritmo de resolucion lineal ordenada sobre
un conjunto de clausulas de Horn, empezaremos siempre por una clausula
negativa (si no existiera podremos afirmar que el conjunto es satisfacible)
y no necesitaremos utilizar literales marcados, ya que todas las resolventes
obtenidas seran igualmente negativas y por lo tanto nunca se podra aplicar el
paso de reduccion.
I. T. en Informatica de Sistemas
28 Logica Computacional
E.T.S.I. Informatica
Logica Computacional: Relacion 5
1. Dada la formula A = ∃x(P (x) → ∀yP (y)), halle un conjunto Ω de
formulas en forma normal de Skolem tal que Ω sea satisfacible si y solo
si lo es A. Determine el universo y la base de Herbrand de Ω y estudie
la satisfacibilidad y la validez de A utilizando el metodo de Gilmore.
2. Para la formula A = ∃x(¬∃yP (x, y) → (∃zQ(z) → R(x))), determine
una formula en forma normal de Skolem equisatisfacible con A y deter-
mine su universo su base de Herbrand. Determine una formula en forma
normal de Skolem equisatisfacible con ¬A y determine su universo y base
de Herbrand.
3. Estudie la validez de la siguientes inferencias utilizando el metodo de
Gilmore:
a)
∃x(P (x) ∧ ∀y(D(y) → L(x, y)))
∀x(P (x) → ∀y(Q(y) → ¬L(x, y)))
∀x(D(x) → ¬Q(x))
b)
∀x∀y∀z((P (x, y) ∧ P (y, z)) → A(x, z))
∀x∃yP (y, x)
∀x∃yA(y, x)
4. Estudie la satisfacibilidad de los siguientes conjuntos usando resolucion
a) p ∨ r ∨ s,¬p ∨ ¬r ∨ s,¬p ∨ r¬s, p¬r ∨ ¬s
b) p ∨ q ∨ r ∨ s,¬q ∨ r ∨ s,¬p ∨ r ∨ s, q ∨ s,¬p ∨ s
c) ¬p ∨ q, q ∨ ¬r ∨ s,¬p ∨ ¬q ∨ r ∨ s,¬r, q
5. Diga si son unificables o no los siguientes pares de atomos y en caso
afirmativo dar el unificador mas general:
Q(f(a), g(x)), Q(y, y)
P (f(x, h(x), y)), P (f(g(z), w, z))
P (a, x, f(g(y))), P (y, f(z), f(z))
P (x, g(f(a)), f(x)), P (f(a), y, y)
P (x, g(f(a)), f(x)), P (f(y), z, y)
P (a, x, f(g(y))), P (z, h(z, u), f(u))
E.T.S.I.Informatica
Tema 5: Resolucion. 29
6. Determine si las siguientes clausulas tienen factores y en tal caso de-
termınelos:
P (x) ∨ Q(y) ∨ P (f(x) P (x) ∨ P (a) ∨ Q(f(x)) ∨ Q(f(a))
P (x, y) ∨ P (a, f(a)) P (a) ∨ P (b) ∨ P (x)
P (x) ∨ P (f(y)) ∨ Q(x, y)
7. Encuentre todas las posibles resolventes, si existen, de los siguientes pares
de clausulas:
¬P (x) ∨ Q(x, b) y P (a) ∨ Q(a, b)
¬P (x) ∨ Q(x, x) y ¬Q(a, f(a))
¬P (x, y, u)∨¬P (y, z, v)∨¬P (x, v,w)∨P (u, z, w), y P (g(x, y), x, y)
¬P (v, z, v) ∨ P (w, z,w) y P (w, h(x, x), w)
8. Estudie la satisfacibilidad de los siguientes conjuntos de clausulas
P (x), Q(x, f(x)) ∨ ¬P (x),¬Q(g(y), z).
Q(a) ∨ R(x),¬Q(x) ∨ R(x),¬R(x) ∨ ¬S(a), S(x).
P (a),¬D(y) ∨ L(a, y),¬P (x) ∨ ¬Q(y) ∨ ¬L(x, y),D(b), Q(b).
P (x, f(x), e),¬S(x) ∨¬S(y)∨¬P (x, f(y), z)∨S(z), S(a),¬S(e).
9. Lea la seccion 5.5 y analice cuales de los conjuntos del ejercicio ante-
rior estan formados por clausulas de Horn. Estudie su satisfacibilidad
atendiendo a las restricciones detalladas en dicha seccion.
I. T. en Informatica de Sistemas
30 Logica Computacional
E.T.S.I. Informatica
Logica Computacional: Ejercicios propuestos (5)
1. Estudie la insatisfacibilidad del siguiente conjunto de clausulas:
M(a, s(c), s(b))
P (a)
M(x, x, s(x))
¬M(x, y, z) ∨ M(y, x, z)
¬M(x, y, z) ∨ D(x, z)
¬P (x) ∨ ¬M(y, z, u) ∨ ¬D(x, u) ∨ D(x, y) ∨ D(x, z)
¬D(a, b)
2. Estudie la insatisfacibilidad del siguiente conjunto de clausulas
P (y, a) ∨ P (f(y), y)
P (y, a) ∨ P (y, f(y))
¬P (x, y) ∨ P (f(y), y)
¬P (x, y) ∨ P (y, f(y))
¬P (x, y) ∨ ¬P (y, a)
3. Estudie la insatisfacibilidad del siguiente conjunto de clausulas:
¬P (x, y, u) ∨ ¬P (y, z, v) ∨ ¬P (x, v,w) ∨ P (u, z, w)
P (g(x, y), x, y)
P (x, h(x, y), y)
¬P (k(x), x, k(x))
4. Para cada una de las formulas siguientes, A: determine una formula en
forma normal de Skolem equisatisfacible con A y determine su universo
y base de Herbrand; determine una formula en forma normal de Skolem
equisatisfacible con ¬A y determine su universo y base de Herbrand.
a) ∀xP (x) → ∃xQ(x)
b) ∀x(P (x) → ∃yR(y))
c) ∀x(P (x) → ∃yQ(x, y))
d) ∃x(¬∃yP (y) → ∃z(Q(z) → R(x)))
e) ∀x∀y(∃zP (z) ∧ ∃u(Q(x, u) → ∃vQ(y, v)))
f ) ∀x∀y(∃z(P (x, z) ∧ P (y, z)) → ∃uQ(x, y, u))
g) ∀x∀y∀z((P (x, y)∧P (y, z)) → Q(x, z))∧(∀x∃yP (x, y) → ∀x∃yQ(x, y))
E.T.S.I.Informatica