Download Índice General 1 Resolución en lógica de proposiciones

Resolución
1
Resolución en lógica de proposiciones
En este apartado se definen los principales conceptos del principio de resolución, pero
sólo a nivel de lógica de proposiciones.
R ESOLUCIÓN
Definición 1 (Resolución binaria, resolvente binario, cláusulas padre) Sean C1 y C2
dos cláusulas con λ ∈ C1 y ¬λ ∈ C2 dos literales complementarios. El procedimiento
de resolución procede como sigue:
César Ignacio García Osorio
1. Borrar λ de C1 y ¬λ de C2 , para dar las cláusulas C1 y C2 .
2. Formar la disyunción C de C1 y C2 .
Índice General
3. Eliminar los posibles literales redundantes de C , para obtener C = (C1 −{λ})∪
(C0 − {¬λ}).
1
Resolución en lógica de proposiciones
1.1 Refutación por resolución . . . . . . . . . . . . . . . . . . . . . . .
2
5
2
Resolución en lógica de predicados
2.1 Refutación por resolución . . . . . . . . . . . . . . . . . . . . . . .
6
9
3
Completitud de la resolución
10
La cláusula resultante C se llama resolvente de C1 y C2 respecto a λ1 , y se denota
por resλ (C1 , C2 ). Las cláusulas C1 y C2 se dice que son las cláusulas padre del resolvente. Esta forma básica de la regla de inferencia resolución también es conocida con
el nombre de resolución binaria, ya que sólo están involucradas dos cláusulas.
4
Agenda
13
Ejemplo 1
Resumen
En este capítulo de presenta los fundamentos teóricos del principio de resolución. El principio de resolución supuso uno de los avances más importantes en
el campo de la demostración automática de teoremas. En este principio ya no se
trabaja de forma explícita con las H-interpretaciones. En vez de generar conjunto
de instancias básicas del conjunto de cláusula original, se trabaja directamente
con las cláusulas. .
Sean las cláusulas C1 = {P }
es:
resλ (C1 , C2 ) =
=
=
y C2 = {¬P, Q}, su resolvente con respecto a P
({P } − {P }) ∪ ({¬P, Q} − {¬P })
∪ {Q}
{Q}.
Si se reescriben las cláusulas como fórmulas bien formadas se comprueba que,
en este ejemplo, la regla de resolución equivale a aplicar la regla modus ponens
sobre las fórmulas originales:
C
¬P → Q
Q
El principio de resolución también puede verse como una extensión de la regla
del literal único de Davis y Putnam.
La resolución tiene la importante propiedad de que cuando dos cláusulas padres
son ciertas bajo una interpretación, su resolvente es también cierto bajo la misma interpretación, por tanto: la resolución es una regla de inferencia sólida . El siguiente
teorema prueba la solidez de la resolución para la lógica de proposiciones.
1
A λ y a ¬λ se les denomina literales de resolución o literales resolventes (del ingles literals resolved
upon).
César I. G. Osorio
2
LSI – Univ. de Burgos
Resolución
Resolución
Teorema 1 Solidez de la resolución en lógica de proposiciones Sean C1 y C2 dos
cláusulas que se pueden resolver y sea C su resolvente, entonces C es consecuencia
lógica de C1 y C2 (C1 , C2 |= C)
Demostración: Si C1 y C2 se pueden resolver existe λ tal que λ ∈ C1 y ¬λ ∈ C2
y se puede escribir:
C1 = {λ} ∪ C1
C2 = {¬λ} ∪ C2
C = C1 ∪ C2
con C1 y C2 cláusulas. Si C1 y C2 son ciertas bajo una interpretación I, se pretende
demostrar que C también es cierta bajo I. Se tiene que λ o ¬λ (uno de los dos) debe ser
falso bajo I. Supóngase que λ es falso bajo I. Entonces C1 no puede ser una cláusula
unitaria, ya que de serlo seria falsa bajo I. Por tanto, C1 debe ser cierto bajo I. De
modo que el resolvente C, es decir C1 ∪ C2 es cierto en I. Análogamente si ¬λ es falso
en I, entonces C2λ debe ser cierto en I. Lo que significa que C1 ∪ C2 debe ser cierto en
I. Con lo que el teorema queda demostrado. En el caso particular de que C1 y C2 sean
cláusulas unitarias se tiene que
C1 = {λ}
C2 = {¬λ}
C=
• Suponemos que Cj es cierto para todo j < i
Si Ci ∈ S, Ci es cierto.
Si Ci ∈
/ S, existen los enteros j < i, k < i y la cláusula λ tales que
Ci = resλ (Cj , Ck ) y entonces Ci es cierto por el teorema 1
Del teorema anterior se deduce que si S es un conjunto de cláusulas inconsistente
entonces existe una derivación por resolución de la cláusula vacía a partir de S. Mas
adelante se verá que si se deriva por resolución la cláusula vacía a partir de un conjunto
de cláusulas S, es porque S es insatisfacible.
A continuación se presentan varios ejemplos en los que se muestra como el principio de resolución puede usarse para probar la insatisfacibilidad de un conjunto de
cláusulas.
Ejemplo 2
Considérese el conjunto de cláusulas:

(1) ¬P ∨ Q 
(2) ¬Q
=S

(3) P
{λ}, {¬λ} |= esto explica el convenio de considerar como inconsistente.
de (1) y (2) se obtiene el resolvente
Definición 2 (Derivación (por resolución), refutación ) Sea S un conjunto de cláusulas y C una cláusula. Una derivación (por resolución) de C a partir de S (S C),
es una secuencia finita de cláusulas C1 , C2 , . . . , Cn , n ≥ 1, tales que Cn = C y para
cada Ck se verifica una de las dos condiciones siguientes:
(4) ¬P
de (4) y (3) se obtiene el resolvente
• Ck es una cláusula de S (Ck ∈ S)
(5) • existen enteros i < k, j < k y un literal λ tales que Ck = resλ (Ci , Cj ). En otras
palabras Ck es un resolvente cuyas cláusulas padre le preceden en la secuencia.
Si Cn = , entonces la derivación se llama refutación (o prueba) de S, e indica
que S es insatisfacible como se muestra en el corolario del siguiente teorema.
Teorema 2 Solidez de la derivación por resolución en lógica de proposiciones Sea
S un conjunto de cláusulas y C una cláusula, si existe una derivación por resolución
de la cláusula C a partir de las cláusulas de S (S C), entonces C es consecuencia
lógica de S (S |= G).
Demostración: Hay que demostrar que si las cláusulas de S son ciertas, entonces
también lo será la cláusula C. Sea C1 , C2 , . . . , Cn = C la derivación por resolución
de la cláusula C a partir de S, la demostración se realizará por inducción sobre las
cláusulas de la derivación. Partimos de que S es cierto y vamos a ver que también lo
es C.
• Por ser S cierto también lo es C1 , ya que (C1 ∈ S).
César I. G. Osorio
3
LSI – Univ. de Burgos
Como se ha derivado por resolución de S, de acuerdo con teorema 2 es
consecuencia lógica de S, y como se verá más adelante esto implica que S es
insatisfacible. Esta no es la única refutación posible de S 2 . En general un conjunto
de cláusulas puede tener más de una refutación3 .
Ejemplo 3
Para el conjunto
(1) P ∨ Q
(2) ¬P ∨ Q
(3) P ∨ ¬Q
(4) ¬P ∨ ¬Q
2







=S
También es posible obtener la derivación por resolución: ¬P ∨ Q, ¬Q, P , Q (de 1 y 3), (de 2 y
4).
3
Como se verá más adelante esto es una de las causas de la ineficiencia de los programas de razonamiento automático. A lo largo de su ejecución se generan cláusulas de más de una refutación, lo ideal
sería generar únicamente las cláusulas de una de ellas, esto el lo que buscan las reglas de inferencia y
las estrategias: disminuir el número de cláusulas generadas la mínimo necesario para generar una única
refutación.
César I. G. Osorio
4
LSI – Univ. de Burgos
Resolución
1.1
¬P ∨ Q
P∨Q
Refutación por resolución
P ∨ ¬Q
Resolución
3. Repetir hasta que se obtenga la cláusula vacía o no se generen nuevas cláusulas:
¬ P ∨ ¬Q
a) Seleccionar dos cláusulas que se puedan resolver, formando su resolvente.
b) Si el resolvente no es la cláusula vacía, añadirlo a S.
¬Q
Q
Como la lógica de proposiciones es decidible, el procedimiento siempre para si le
asignamos suficientes recursos. Cuando termina hay dos posibilidades:
i) Se ha generado la cláusula vacía, lo que significa que S es inconsistente, es decir,
S0 ∪ {¬t} es inconsistente, luego S0 |= t y t es un teorema de T (sistema formal
completo).
ii) No se generan nuevos resolventes, lo que significa que S es consistente, es decir
S0 ∪{¬t} es consistente, luego S0 |= t y t no es un teorema de T (sistema formal
sólido).
Figura 1: Grafo/árbol de derivación
se puede generar los siguientes resolventes
(5) Q
de (1) y (2)
(6) ¬Q de (3) y (4)
(7) de (5) y (6)
Como se ha derivado , S es insatisfacible.
Una derivación como la anterior puede ser representada en un grafo llamado grafo
de derivación, que se muestra en la figura 1. En el caso de una refutación, los vértices
en el grafo de derivación están restringidos a ser aquellas cláusulas que intervienen
directa o indirectamente en la refutación en la refutación. Este grafo de derivación
toma la forma de un árbol y usualmente se usa el termino árbol de derivación para
designarlo. Las hojas de este árbol son las cláusulas del conjunto original, y la raíz del
árbol es la cláusula vacía (o, si en vez de una refutación se trata de una derivación,
la cláusula derivada).
1.1
Refutación por resolución
A continuación se verán los pasos que hay que dar para probar un teorema de una
teoría mediante el uso de la refutación y de la resolución como regla de inferencia.
La refutación por resolución consiste en realizar una demostración por refutación
empleando la resolución como única regla de inferencia.
Para probar que t es un teorema de una teoría T sobre un sistema formal axiomático
sólido y completo, se usa el siguiente procedimiento:
1. Convertir los axiomas de T a forma normal conjuntiva. Crear el conjunto S0 con
todas las fórmulas obtenidas.
2. Negar t y convertirlo a forma normal conjuntiva. Añadir las cláusulas obtenidas
a S0 , obteniendo S.
César I. G. Osorio
5
LSI – Univ. de Burgos
Si no se exige un sistema formal sólido y completo, el procedimiento sólo demuestra la consistencia o inconsistencia de S.
El principio de resolución es una regla de inferencia potente. En la siguiente sección se definirá este principio para la lógica de primer orden. Se verá además la completitud del principio de resolución, es decir si un conjunto de cláusulas es insatisfacible se podrá derivar la cláusula vacía utilizando la resolución.
2
Resolución en lógica de predicados
El mismo principio de resolución aplicable a la lógica de proposiciones, es aplicable a
la de predicados. Para poder aplicar el principio de resolución a la lógica de predicados
se necesita, sin embargo, introducir el concepto de unificación. Básicamente la unificación es un algoritmo que permite calcular la sustitución de variables por términos
que hace que dos expresiones sean sintácticamente iguales. La unificación se explica
en detalle en el anexo I, que es conveniente haber leído para entender lo que aquí se
explica, no obstante se va a dar una idea general de como se usa este concepto en la
obtención de resolventes a través de un par de ejemplos.
Ejemplo 4
Se tienen la fórmulas:
(∀x)(∀y)(¬P (x, g(y)) ∨ Q(x))
(∀v)P (a, v)
Se quiere aplicar la regla de inferencia modus ponens pero tal como están la
fórmulas no podemos, pero como se tiene el mismo predicado y los cuantificadores universales, se pueden manipular las fórmulas para conseguir la aplicación de
la regla de inferencia.
César I. G. Osorio
6
LSI – Univ. de Burgos
Resolución
Resolución
La manipulación consistirá en la sustitución de las variables por términos mediante el uso de la regla de inferencia de instanciación universal. Se sustituye la
variable x de la primera fórmula por el termino a y la variable v de la segunda
por el termino g(y), para obtener la fórmulas
¬P (a, g(y)) ∨ Q(a)
P (a, g(y))
sobre las que si se puede aplicar la regla de inferencia modus ponens para concluir
finalmente:
Definición 3 (Resolvente binario, cláusulas padre, literales de resolución) Sean C1
y C2 dos cláusulas que no tienen variables comunes5 . Sean L1 ∈ C1 y L2 ∈ C2
dos literales de manera que L1 y ¬L2 sean unificables con unificador más general θ.
Se denomina resolvente binario de C1 y C2 (respecto a L1 y L2 ) y se denota, por
resL1 ,L2 (C1 , C2 ) a la cláusula:
resL1 ,L2 (C1 , C2 ) = (C1 θ − {L1 }θ) ∪ (C2 θ − {L2 }θ)
Las cláusulas C1 y C2 se llaman cláusulas padres de resL1 ,L2 (C1 , C2 ). Y los literales
L1 y L2 se llaman literales de resolución (literals resolved upon).
Q(a)
Ejemplo 5
Ejemplo 6
Sea el conjunto de cláusulas:
(1)
(2)
(3)
(4)
A continuación se definen los conceptos relativos al principio de resolución para la
lógica de primer orden (algunos de ellos son similares, pero otros son nuevos para la
lógica de predicados).
Sean C1 = P (x) ∨ Q(x) y C2 = ¬P (a) ∨ R(x). Como x aparece en las dos
cláusulas se renombra la variable en C2 para tener C2 = ¬P (a) ∨ R(y). Los
literales de resolución son L1 = P (x) y L2 = ¬P (a). Como L1 y ¬L2 son
unificables con unificador más general θ = {a/x} se tiene que
P (x1 ) ∨ Q(x1 , y1 )
¬P (a) ∨ Q(x2 , f (y2 ))
P (b) ∨ Q(x3 , y3 )
¬P (y4 ) ∨ ¬Q(x4 , f (y4 ))
a partir de este conjunto de cláusulas se puede obtener una serie de “resolventes”
si se combina la resolución con la sustitución de variables por términos4 .
resL1 ,L2 (C1 , C2 ) =
=
=
=
(C1 θ − {L1 }θ) ∪ (C2 θ − {L2 }θ)
({P (a), Q(a)} − {P (a)}) ∪ ({¬P (a), R(y)} − {¬P (a)})
{Q(a)} ∪ {R(y)}
{Q(a), R(y)}
por tanto Q(a) ∨ R(y) es un resolvente binario de C1 y C2 .
(5)
P (a) ∨ Q(a, f (y2 ))
(6)
(7)
(8)
(9)
¬P (a) ∨ Q(a, f (y2 ))
Q(a, f (y2 ))
P (b) ∨ Q(x3 , f (y4 ))
¬P (b) ∨ ¬Q(x3 , f (y4 ))
(10)
(11)
(12)
(13)
¬Q(x3 , f (b))
Q(a, f (b))
¬Q(a, f (b))
de (1) al sustituir la variable x1 por el termino constante a,
y la variable y1 por el termino f (y2 )
de (2) al sustituir la variable x2 por el termino constante a
de (1) y (2) aplicando la resolución
de (3) al sustituir la variable y3 por el termino f (y4 )
de (4) al sustituir la variable y4 por el termino b, y la variable x4 por el termino x3
de (8) y (9) aplicando la resolución
de (7) al sustituir la variable y2 por el termino b
de (10) al sustituir la variable x3 por el termino a
de (11) y (12) aplicando la resolución
como finalmente se obtiene la cláusula vacía a partir de S, S es inconsistente.
Ejemplo 7
Sean C1 = P (x, x) y C2 = ¬P (y, f (y)), como P (x, x) y ¬P (y, f (y)) no son
unificables C1 y C2 no se pueden resolver.
Definición 4 (Factor, factor unitario, factorización) Si dos o más literales (con el
mismo signo) de una cláusula C tienen un unificador más general θ, entonces Cθ se
llama factor de C. Si Cθ es una cláusula unitaria, Cθ se llama factor unitario de C. Al
proceso de obtener el factor de una cláusula se le denomina factorización.
Ejemplo 8
Sea C = P (x) ∨ P (f (y)) ∨ ¬Q(x). Los literales primero y segundo son unificables con unificador más general θ = {f (y)/x}. Por tanto, Cθ = P (f (y)) ∨
¬Q(f (y)) es un factor de C.
Como se ve las cláusulas del ejemplo no tienen variables comunes. Si el conjunto inicial de cláusulas tuviera cláusulas con variables comunes, lo habitual es renombrar la variables comunes para deshacer
esta situación, a esta operación de renombrado se la llama normalización por separado. Esta operación
es posible ya que las variables son mudas y sólo tienen relevancia en la cláusula en la que aparecen,
es decir, una variable llamada x que aparece en una cláusula no tiene nada que ver con una variable
llamada x que aparezca en otra cláusula.
Definición 5 (Resolvente) Sean C1 y C2 dos cláusulas que no tienen variables comunes. Se denomina resolvente de las cláusulas (padre) C1 y C2 a cualquiera de los
siguientes resolventes binarios:
César I. G. Osorio
César I. G. Osorio
4
7
LSI – Univ. de Burgos
5
Si tuvieran variables comunes, habría que renombrar las variables para que eso no sucediera (ver
nota anterior).
8
LSI – Univ. de Burgos
Resolución
2.1
Refutación por resolución
Resolución
1. resolvente binario de C1 y C2 .
procedure Resolución(S)
cláusulas← S;
while ∈
/ cláusulas do
{Ci , Cj }←SeleccionarClausulasAResolver(cláusulas);
resolvente←Resolver(Ci , Cj );
cláusulas←cláusulas ∪{resolvente};
end_while
end
2. resolvente binario de C1 y un factor de C2 .
3. resolvente binario de un factor de C1 y C2 .
4. resolvente binario de un factor de C1 y un factor de C2 .
Ejemplo 9
Sean C1 = P (x) ∨ P (f (y)) ∨ R(g(y)) y C2 = ¬P (f (g(a))) ∨ Q(b). Un factor de C1 es C1 = P (f (y)) ∨ R(g(y)). Un resolvente binario de C1 y C2 es
R(g(g(a))) ∨ Q(b). De modo que R(g(g(a))) ∨ Q(b) es un resolvente de C1 y
C2 .
Las condiciones de terminación para la lógica de predicados son como se ve algo
diferentes, esto es debido al hecho de que la lógica de predicados no es decidible. Las
posibilidades que se tienen son:
Ejemplo 10
Sean C1 = P (x)∨P (y) y C2 = ¬P (u)∨¬P (v). Un factor de C1 es C1 = P (x) y
un factor de C2 es C2 = ¬P (u). El resolvente binario de C1 y C2 es , por tanto
es un resolvente de C1 y C2 . Claramente el conjunto {C1 , C2 } es inconsistente
pero la resolución binaria sin la factorización no permite obtener la cláusula vacía.
i) Se ha generado la cláusula vacía:
Los teoremas teorema 1 y teorema 2 vistos para la lógica de proposiciones se cumplen también para la de predicados pero utilizando la operación de resolución aquí
definida. La demostración de estos teoremas se traslada de forma inmediata a la lógica
de predicados. Del mismo modo es valida la definición de derivación y de refutación
pero como antes considerando la operación de resolución definida en la definición 5.
ii) No se generan nuevos resolventes:
2.1
S inconsistente, S0 ∪ {¬t} inconsistente, luego S0 |= t y t es un teorema de T
(sistema formal completo).
S es consistente, S0 ∪ {¬t} consistente, luego S0 |= t y t no es un teorema de T
(sistema formal sólido).
iii) Se agotan los recursos asignados: no se puede concluir nada
– S consistente: se pueden generar infinitos resolventes sin obtener .
Refutación por resolución
– S inconsistente: podemos generar sin más que aumentar los recursos.
El procedimiento de refutación por resolución visto para la lógica de proposiciones
también se puede utilizar para la lógica de predicados. Para probar que t es un teorema de una teoría T sobre un sistema formal axiomático sólido y completo, se usa el
siguiente procedimiento:
1. Convertir los axiomas de T a forma clausulada. Llama S0 al conjunto formado
con todas las cláusulas obtenidas.
2. Negar t y convertirlo a forma clausulada. Añadir las cláusulas obtenidas a S0 ,
obteniendo S.
3. Repetir hasta que se obtenga la cláusula vacía, no se generen nuevas cláusulas o
se consuman los recursos asignados:
a) Seleccionar dos cláusulas que se puedan resolver, formando su resolvente.
b) Si el resolvente no es la cláusula vacía, añadirlo a S. Si se obvian las dos
condiciones de finalización relativa al consumo de recursos y a la imposibilidad de generación de cláusulas, este último paso se puede poner en una
notación más próxima a los lenguaje de programación como:
César I. G. Osorio
9
LSI – Univ. de Burgos
3
Completitud de la resolución
En el teorema 1 se afirmaba que la resolución era una regla de inferencia sólida (si
un conjunto S de cláusulas es insatisfacible se va a poder derivar la cláusula vacía a
partir de S utilizando la resolución como única regla de inferencia). Aquí se verá que
además es una regla de inferencia completa (si se deriva la cláusula vacía a partir de
un conjunto de cláusulas S utilizando la resolución como regla de inferencia, S es
insatisfacible). Para ello son necesarias las definiciones de los conceptos de número de
ocurrencias de literales en una forma cláusulas y de número de literales en exceso, y
la demostración del teorema de completitud básica. Además es necesario el teorema
de “lifting” que nos permite pasar del resultado de completitud para cláusulas básicas
a la completitud para cláusulas no básicas.
Definición 6 (Número de ocurrencias de literales) Se denomina número de ocurrencias de literales en una forma clausulada a la suma de ocurrencias de literales de cada
cláusula.
César I. G. Osorio
10
LSI – Univ. de Burgos
Resolución
Resolución
Definición 7 (Número de literales en exceso ) Se denomina número de literales en
exceso de una forma clausulada al número de ocurrencias de literales menos el número
de cláusulas.
Teorema 4 Lema de “lifting” Sean C1 y C2 dos cláusulas que no tienen variables
comunes y C1 y C2 particularizaciones básicas de C1 y C2 respectivamente. Si C es
un resolvente de C1 y C2 , entonces existe un resolvente C de C1 y C2 tal que C es una
particularización básica de C.
Demostración: En primer, lugar si fuera necesario, se renombran las variables de
C1 y C2 para que no haya variables en común. Sean L1 y L2 los literales de resolución
y
C = (C1 γ − {L1 }γ) ∪ (C2 γ − {L2 }γ)
Ejemplo 11
Ejemplo 1.11 Sea el conjunto de cláusulas S = {P ∨ Q, ¬P ∨ R, Q} se tienen
que:
• su número de literales es: 2 + 2 + 1 = 5.
• su número de literales en exceso es: 5 − 3 = 2.
Teorema 3 Teorema de completitud básica Sea S un conjunto finito de cláusulas
básicas. Si S es insatisfacible, existe una derivación por resolución de la cláusula vacía
a partir de S.
Demostración: Sea S un conjunto inconsistente de cláusulas básicas.
i) Si ∈ S, se deriva trivialmente de S.
ii) Si ∈
/ S, la existencia de la derivación de a partir de S se demuestra por inducción sobre el número de literales en exceso de S. Sea n el número de literales
en exceso de S.
– Si n = 0, todas las cláusulas de S son unitarias, como se tiene que ∈
/
S la única forma de que S sea inconsistente es que existan dos literales
complementarios, a partir de los cuales se obtiene .
– Se supone que el teorema se cumple para n = k−1(k > 0). Para n = k > 0
existe al menos una cláusula C con más de un literal ( ∈
/ S), se selecciona
un literal λ ∈ C, se forma C = C − {λ} y se crean dos nuevas forma
clausuladas.
S1 = (S − {C}) ∪ {C }
S2 = (S − {C}) ∪ {{λ}}
Si S es inconsistente, S1 y S2 son inconsistentes6 . Como el número de
literales en exceso de S1 y S2 es menor que n, por la hipótesis de inducción
podemos derivar la cláusula vacía tanto de S1 como de S2 .
Considérese la derivación a partir de S1 .
∗ Si C no se usa en esta derivación, se tiene una derivación de a partir
de S.
∗ Si C se usa, se realiza la siguiente construcción:
1. Añadir λ en C y sus descendientes en la derivación a partir de S1 .
2. Si sigue perteneciendo a la secuencia, ya esta. En caso contrario,
en vez de la cláusula se tendrá la cláusula {λ}. Añadiendo la
derivación de a partir de S2 a esta derivación de {λ}, se tendrá
una derivación de a partir de S.
6
Esto se sigue por un razonamiento similar al que se vio para la reglas de Davis y Putnam
César I. G. Osorio
11
LSI – Univ. de Burgos
donde γ es un unificador más general de L1 y L2 . Dado que C1 y C2 son instancias de
C1 y de C2 , existe la sustitución θ tal que C1 θ = C1 y C2 θ = C2 . Sean L11 , L2i , . . . , Lri i
los literales de Ci correspondientes al literal Li (es decir L1i θ = L2i θ = . . . = Lri i θ),
para i = 1, 2. Si ri > 1, se obtiene el unificador más general λi de {L1i , L2i , . . . , Lri i } y
sea Li = L1i λi , para i = 1, 27 . Se tiene que Li es un literal en el factor Ci λi de Ci . Si
ri = 1, se hace que λi sea λi = y Li = L1i λi . Sea λ = λ1 ∪ λ2 8 , entonces claramente
Li es una instancia de Li 9 . Dado que L1 y ¬L2 son unificables, también lo son L1 y
¬L2 . Sea σ el unificador más general de L1 y ¬L2 , y
C = ((C1 λ)σ − L1 σ) ∪ ((C2 λ)σ − L2 σ)
= ((C1 λ)σ − ({L11 , L21 , . . . , Lr11 }λ)σ) ∪ ((C2 λ)σ − ({L12 , L22 , . . . , Lr22 }λ)σ)
= (C1 (λ ◦ σ) − ({L11 , L21 , . . . , Lr11 }(λ ◦ σ)) ∪ (C2 (λ ◦ σ) − ({L12 , L22 , . . . , Lr22 }(λ ◦ σ))
C es un resolvente de C1 y C2 . Claramente, C es una instancia de C puesto que
C = (C1 γ − L1 γ) ∪ (C2 γ − L2 γ)
r2
1
2
= ((C1 θ)γ − ({L11 , L21 , . . . , Lr1
1 }θ)γ) ∪ ((C2 θ)γ − ({L2 , L2 , . . . , L2 }θ)γ)
= (C1 (θ ◦ γ) − ({L11 , L21 , . . . , Lr11 }(θ ◦ γ)) ∪ (C2 (θ ◦ γ) − ({L12 , L22 , . . . , Lr22 }(θ ◦ γ))
y (λ◦σ) es más general que (θ ◦γ)10 , con lo que se completa la demostración del lema.
Teorema 5 Teorema de “lifting” Sea S una forma clausulada y S un conjunto de
particularizaciones básicas de cláusulas de S. si existe una derivación por resolución
de la cláusula C a partir de S , existe una derivación por resolución de la cláusula C a
partir de S y C es una particularización básica de C.
L1i λi , L2i λi , . . . , Lri i λi son el mismo literal ya que λi es el unificador más general.
Esta operación es una simple unión sin mas, dado que al haber renombrado las variables de C1 y
de C2 las variables ligadas de las sustituciones de λ1 y λ2 no van a ser las mismas. Se tiene por tanto
que L1i λ = L1i λi = Li , para i = 1, 2.
9
Recuérdese que Li se ha construido a partir de los literales L1i , L2i , . . . , Lri i , mediante la unificación
de los mismos.
10
(λ ◦ σ) es más general que (θ ◦ γ) ya que la aplicación de (θ ◦ γ) sobre C1 y C2 da como resultado
instancias básicas, mientras que la aplicación de (λ ◦ σ) no tiene por que (por otro lado recuérdese que
σ es un unificador más general). Por ser (λ ◦ σ) más general que (θ ◦ γ) debe existir una sustitución µ
tal que (θ ◦ γ) = (θ ◦ γ) ◦ µ, y por tanto C = Cµ .
7
8
César I. G. Osorio
12
LSI – Univ. de Burgos
Resolución
Resolución
REFERENCIAS
Finalmente se esta en condiciones de enunciar el teorema de completitud que junto
con el teorema 2 nos permiten asegurar la solidez y completitud del procedimiento de
refutación por resolución.
[WOB91] Larry Wos, Ewing Overbeek, Ross adn Lusk, y Jim Boyle. Automated
Reasoning: Introduction and Aplications. McGraw-Hill, 1991.
Teorema 6 Teorema de completitud Sea S un conjunto finito de cláusulas. Si S es
insatisfacible, existe una derivación por resolución de la cláusula vacía a partir de S.
Demostración: Si S es insatisfacible, por el teorema de Herbrand, existe un conjunto de particularizaciones básicas de S, S que es insatisfacible (subconjunto de su
expansión de Herbrand). Si S es insatisfacible, el teorema de completitud básica garantiza que existe una derivación por resolución de la cláusula vacía a partir de S . Por
el teorema de lifting, podemos convertir esta derivación en una derivación de a partir
de S.
4 Agenda
Este capítulo junto con el anterior es uno de los más importantes. Si en el capítulo
anterior se daban la parte más importante de los conceptos teóricos para asentar los
principios en los que se basa la demostración automática de teoremas, en este capítulo aparece una regla de inferencia que hace que la demostración sea algo práctico. El
principio de resolución supone un cambio cualitativo en la forma de resolver los problemas de demostración automática de teoremas. Antes de formularse este principio
la demostración pasaba por la generación a partir del conjunto de cláusulas inicial de
conjuntos de cláusulas básicas, entonces se utilizaba este conjunto para intentar probar
la satisfacibilidad o insatisfacibilidad del conjunto original. Con la regla de resolución
se pasa a trabajar directamente con el conjunto dado. Además la eficiencia es mucho
mayor. Sin con la introducción de las H-interpretaciones se había eliminado en parte la
dependencia semántica de las fórmulas de la lógica de primer orden, al tener que considerar únicamente una interpretación especifica, con el principio de resolución esta
dependencia es mucho menor al no considerar ninguna interpretación de forma explícita. Por otra parte el principio de resolución ha sido la base del desarrollo de otras
reglas de inferencia posteriores todavía más eficientes. Si hoy en día la demostración
automática de teoremas es algo factible, es gracias al principio de resolución.
Referencias
[CCT73]
Chin-Liang Chang y Lee Richard Char-Tung. Symbolic Logic and Mechanical Theorem Proving. Computer science classics. Academic Press,
1973.
[LVDG91] Peter Lucas y Linda Van Der Gaag. Principles of expert systems. AddisonWesley, 1991.
César I. G. Osorio
13
LSI – Univ. de Burgos
César I. G. Osorio
14
LSI – Univ. de Burgos