Resolución en lógica de primer orden

Paradigmas de Lenguajes de Programación

Forma clausal

I Es una forma normal conjuntiva, en notación de conjuntos.

I Análogo a la forma clausal del marco proposicional.
I Pero requiere tener en cuenta los cuantificadores.
Forma clausal

I Es una forma normal conjuntiva, en notación de conjuntos.

I Análogo a la forma clausal del marco proposicional.
I Pero requiere tener en cuenta los cuantificadores.
I El pasaje a forma clausal consiste en seis pasos de conversión.
1. Escribir la fórmula en términos de ∧, ∨, ¬, ∀, ∃ (i.e. eliminar
implicación).
2. Pasar a forma normal negada.
3. Pasar a forma normal prenexa (opcional).
4. Pasar a forma normal de Skolem.
5. Pasar matriz a forma normal conjuntiva.
6. Distribuir cuantificadores universales.
Forma normal negada

El conjunto de fórmulas en forma normal negada (FNN) se define

inductivamente como:
1. Para cada fórmula atómica A, A y ¬A están en FNN.
2. Si A, B ∈ FNN, entonces (A ∨ B), (A ∧ B) ∈ FNN.
3. Si A ∈ FNN, entonces ∀x.A, ∃x.A ∈ FNN.
Forma normal negada

El conjunto de fórmulas en forma normal negada (FNN) se define

inductivamente como:
1. Para cada fórmula atómica A, A y ¬A están en FNN.
2. Si A, B ∈ FNN, entonces (A ∨ B), (A ∧ B) ∈ FNN.
3. Si A ∈ FNN, entonces ∀x.A, ∃x.A ∈ FNN.

Ejemplos
I ¬∃x.((P(x) ∨ ∃y .R(x, y )) ⊃ (∃z.R(x, z) ∨ P(a)))
Forma normal negada

El conjunto de fórmulas en forma normal negada (FNN) se define

inductivamente como:
1. Para cada fórmula atómica A, A y ¬A están en FNN.
2. Si A, B ∈ FNN, entonces (A ∨ B), (A ∧ B) ∈ FNN.
3. Si A ∈ FNN, entonces ∀x.A, ∃x.A ∈ FNN.

Ejemplos
I ¬∃x.((P(x) ∨ ∃y .R(x, y )) ⊃ (∃z.R(x, z) ∨ P(a)))no está en
FNN.
I ∀x.((P(x) ∨ ∃y .R(x, y )) ∧ (∀z.¬R(x, z) ∧ ¬P(a)))
Forma normal negada

El conjunto de fórmulas en forma normal negada (FNN) se define

inductivamente como:
1. Para cada fórmula atómica A, A y ¬A están en FNN.
2. Si A, B ∈ FNN, entonces (A ∨ B), (A ∧ B) ∈ FNN.
3. Si A ∈ FNN, entonces ∀x.A, ∃x.A ∈ FNN.

Ejemplos
I ¬∃x.((P(x) ∨ ∃y .R(x, y )) ⊃ (∃z.R(x, z) ∨ P(a)))no está en
FNN.
I ∀x.((P(x) ∨ ∃y .R(x, y )) ∧ (∀z.¬R(x, z) ∧ ¬P(a)))está en
FNN.
Forma normal negada
Toda fórmula es lógicamente equivalente a otra en FNN.
Forma normal negada
Toda fórmula es lógicamente equivalente a otra en FNN.
Dem.
Por inducción estructural usando:
¬(A ∧ B) ⇐⇒ ¬A ∨ ¬B
¬(A ∨ B) ⇐⇒ ¬A ∧ ¬B
¬¬A ⇐⇒ A
¬∀x.A ⇐⇒ ∃x.¬A
¬∃x.A ⇐⇒ ∀x.¬A
Forma normal negada
Toda fórmula es lógicamente equivalente a otra en FNN.
Dem.
Por inducción estructural usando:
¬(A ∧ B) ⇐⇒ ¬A ∨ ¬B
¬(A ∨ B) ⇐⇒ ¬A ∧ ¬B
¬¬A ⇐⇒ A
¬∀x.A ⇐⇒ ∃x.¬A
¬∃x.A ⇐⇒ ∀x.¬A

Ejemplos
I ¬∃x.(¬(P(x) ∨ ∃y .R(x, y )) ∨ (∃z.R(x, z) ∨ P(a))) se
transforma en
Forma normal negada
Toda fórmula es lógicamente equivalente a otra en FNN.
Dem.
Por inducción estructural usando:
¬(A ∧ B) ⇐⇒ ¬A ∨ ¬B
¬(A ∨ B) ⇐⇒ ¬A ∧ ¬B
¬¬A ⇐⇒ A
¬∀x.A ⇐⇒ ∃x.¬A
¬∃x.A ⇐⇒ ∀x.¬A

Ejemplos
I ¬∃x.(¬(P(x) ∨ ∃y .R(x, y )) ∨ (∃z.R(x, z) ∨ P(a))) se
transforma en
I ∀x.((P(x) ∨ ∃y .R(x, y )) ∧ (∀z.¬R(x, z) ∧ ¬P(a)))
Forma normal prenexa

Fórmula de la forma Q1 x1 . . . Qn xn .B, n ≥ 0, donde

I B sin cuantificadores (llamada matriz)
I x1 , . . . , xn son variables
I Qi ∈ {∀, ∃}
Forma prenexa

Toda fórmula rectificada A es lógicamente equivalente a una

fórmula B en forma prenexa.
Forma prenexa

Toda fórmula rectificada A es lógicamente equivalente a una

fórmula B en forma prenexa.
Demostración
Por inducción estructural usando:
(∀x.A) ∧ B ⇐⇒ ∀x.(A ∧ B) (∀x.A) ∨ B ⇐⇒ ∀x.(A ∨ B)
(A ∧ ∀x.B) ⇐⇒ ∀x.(A ∧ B) (A ∨ ∀x.B) ⇐⇒ ∀x.(A ∨ B)
(∃x.A) ∧ B ⇐⇒ ∃x.(A ∧ B) (∃x.A) ∨ B ⇐⇒ ∃x.(A ∨ B)
(A ∧ ∃x.B) ⇐⇒ ∃x.(A ∧ B) (A ∨ ∃x.B) ⇐⇒ ∃x.(A ∨ B)

I Nota: Con estas equivalencias basta, si asumimos que A está

en FNN.
Ejemplo

1. ∀x.¬P(x) ∧ (∃y .Q(y ) ∨ ∀z.P(z))

Ejemplo

1. ∀x.¬P(x) ∧ (∃y .Q(y ) ∨ ∀z.P(z))

2. ∀x.¬P(x) ∧ (∃y .(Q(y ) ∨ ∀z.P(z)))
Ejemplo

1. ∀x.¬P(x) ∧ (∃y .Q(y ) ∨ ∀z.P(z))

2. ∀x.¬P(x) ∧ (∃y .(Q(y ) ∨ ∀z.P(z)))
3. ∃y .(∀x.¬P(x) ∧ (Q(y ) ∨ ∀z.P(z)))
Ejemplo

1. ∀x.¬P(x) ∧ (∃y .Q(y ) ∨ ∀z.P(z))

2. ∀x.¬P(x) ∧ (∃y .(Q(y ) ∨ ∀z.P(z)))
3. ∃y .(∀x.¬P(x) ∧ (Q(y ) ∨ ∀z.P(z)))
4. ∃y .(∀x.¬P(x) ∧ ∀z.(Q(y ) ∨ P(z)))
Ejemplo

1. ∀x.¬P(x) ∧ (∃y .Q(y ) ∨ ∀z.P(z))

2. ∀x.¬P(x) ∧ (∃y .(Q(y ) ∨ ∀z.P(z)))
3. ∃y .(∀x.¬P(x) ∧ (Q(y ) ∨ ∀z.P(z)))
4. ∃y .(∀x.¬P(x) ∧ ∀z.(Q(y ) ∨ P(z)))
5. ∃y .∀z.(∀x.¬P(x) ∧ (Q(y ) ∨ P(z)))
Ejemplo

1. ∀x.¬P(x) ∧ (∃y .Q(y ) ∨ ∀z.P(z))

2. ∀x.¬P(x) ∧ (∃y .(Q(y ) ∨ ∀z.P(z)))
3. ∃y .(∀x.¬P(x) ∧ (Q(y ) ∨ ∀z.P(z)))
4. ∃y .(∀x.¬P(x) ∧ ∀z.(Q(y ) ∨ P(z)))
5. ∃y .∀z.(∀x.¬P(x) ∧ (Q(y ) ∨ P(z)))
6. ∃y .∀z.∀x.(¬P(x) ∧ (Q(y ) ∨ P(z)))
Forma normal de Skolem

I Hasta ahora tenemos una fórmula que:

1. está escrita en términos de ∧, ∨, ¬, ∀, ∃,
2. si tiene negaciones, solamente se aplican a átomos (forma
normal negada),
3. (opcionalmente) si tiene cuantificadores, se encuentran todos
en el prefijo (forma normal prenexa).
I El proceso de pasar una fórmula a forma normal de Skolem se
llama skolemización.
I El objetivo de la skolemización es
1. eliminar los cuantificadores existenciales
2. sin alterar la satisfactibilidad.
Eliminación de cuantificadores existenciales
Eliminación de cuantificadores existenciales

I ¿Cómo eliminamos los ∃ sin cambiar la satisfactibilidad?

Eliminación de cuantificadores existenciales

I ¿Cómo eliminamos los ∃ sin cambiar la satisfactibilidad?

I Introducimos “testigos” para ellos.
I Todo cuantificador existencial se instancia en una constante o
función de skolem.
Eliminación de cuantificadores existenciales

I ¿Cómo eliminamos los ∃ sin cambiar la satisfactibilidad?

I Introducimos “testigos” para ellos.
I Todo cuantificador existencial se instancia en una constante o
función de skolem.
I Ejemplo: ∃x.P(x) se skolemiza a P(c) donde c es una nueva
constante que se agrega al lenguaje de primer orden.
I Estas funciones y constantes se suelen conocer como
parámetros.
¿Cómo se altera el significado de la fórmula?

Prop.
Si A0 es el resultado de skolemizar A, entonces A es satisfactible sii
A0 es satisfactible.
I Consecuencia: La skolemización preserva insatisfactibilidad.
I Esto es suficiente para poder aplicar el método de resolución,
tal como veremos.
¿Preservación de validez?

I ¿Podremos eliminar los cuantificadores existenciales, usando

skolemización, sin alterar la validez?
¿Preservación de validez?

I ¿Podremos eliminar los cuantificadores existenciales, usando

skolemización, sin alterar la validez?
I Esto es mucho más fuerte que preservar satisfactibilidad...
I Respuesta: No.
I Ejemplo: ∃x.(P(a) ⊃ P(x)) es válida pero P(a) ⊃ P(b) no lo
es.
I Tal como se mencionó, la skolemización sı́ preserva
satisfactibilidad y ello es suficiente para el método de
resolución.
Skolemización
Cada ocurrencia de una subfórmula

∃x.B

en A se reemplaza por

B{x ← f (x1 , . . . , xn )}

donde
I •{• ← •} es la operación usual de sustitución (sustituir todas
las ocurrencias libres de una variable en una expresión -
fórmula o término - por otra expresión).
I f es un sı́mbolo de función nuevo y las x1 , . . . , xn son las
variables de las que depende x en B.
I Si ∃x.B forma parte de una fórmula mayor, x solo depende de
las variables libres de B (por ejemplo, en ∀z.∀y .∃x.P(y , x) la
x depende de y ).
Definición de forma normal de Skolem (1/2)

I Sea A una sentencia rectificada en FNN.

I No es necesario que esté en forma prenexa.
I Una forma normal de Skolem de A (escrito SK(A)) es una
fórmula sin existenciales que se obtiene recursivamente como
sigue.
I Sea A0 cualquier subfórmula de A.
I Si A0 es una fórmula atómica o su negación, SK(A0 ) = A0 .
I Si A0 es de la forma (B ? C ) con ? ∈ {∨, ∧}, entonces
SK(A0 ) = (SK(B) ? SK(C )).
I Si A0 es de la forma ∀x.B, entonces SK(A0 ) = ∀x.SK(B).
I Sigue en siguiente diapositiva.
Definición de forma normal de Skolem (2/2)

I Si A0 es de la forma ∃x.B y {x, y1 , . . . , ym } son las variables

libres de B 1 , entonces
1. Si m > 0, crear un nuevo sı́mbolo de función de Skolem, fx de
aridad m y definir
SK(A0 )=SK(B{x ← fx (y1 , . . . , ym )})
2. Si m = 0, crear una nueva constante de Skolem cx y
SK(A0 )=SK(B{x ← cx })
Nota: dado que A está rectificada, cada fx y cx es única.

1
Notar que se ligan en A dado que A es sentencia
Ejemplos

Considerar
 la fórmula 
∀x. P(a) ∨ ∃y .(Q(y ) ∧ ∀z.(P(y , z) ∨ ∃u.Q(x, u))) ∨ ∃w .Q(w )
La forma normal de Skolem es:
∀x.(P(a) ∨ (Q(g (x)) ∧ ∀z.(P(g (x), z) ∨ Q(x, f (x))))) ∨ Q(c)
Ejemplos

I Considere la sentencia:
∀x.∃y .∃z.R(x, y , z)
1. Alternativa 1 (rojo, azul)
Ejemplos

I Considere la sentencia:
∀x.∃y .∃z.R(x, y , z)
1. Alternativa 1 (rojo, azul)
1.1 ∀x.∃y .∃z.R(x, y , z)
1.2 ∀x.∃z.R(x, f (x), z)
Ejemplos

I Considere la sentencia:
∀x.∃y .∃z.R(x, y , z)
1. Alternativa 1 (rojo, azul)
1.1 ∀x.∃y .∃z.R(x, y , z)
1.2 ∀x.∃z.R(x, f (x), z)
1.3 ∀x.R(x, f (x), g (x))
Ejemplos

I Considere la sentencia:
∀x.∃y .∃z.R(x, y , z)
1. Alternativa 1 (rojo, azul)
1.1 ∀x.∃y .∃z.R(x, y , z)
1.2 ∀x.∃z.R(x, f (x), z)
1.3 ∀x.R(x, f (x), g (x))
2. Alternativa 2 (azul, rojo)
Ejemplos

I Considere la sentencia:
∀x.∃y .∃z.R(x, y , z)
1. Alternativa 1 (rojo, azul)
1.1 ∀x.∃y .∃z.R(x, y , z)
1.2 ∀x.∃z.R(x, f (x), z)
1.3 ∀x.R(x, f (x), g (x))
2. Alternativa 2 (azul, rojo)
2.1 ∀x.∃y .∃z.R(x, y , z)
2.2 ∀x.∃y .R(x, y , h(x, y ))
Ejemplos

I Considere la sentencia:
∀x.∃y .∃z.R(x, y , z)
1. Alternativa 1 (rojo, azul)
1.1 ∀x.∃y .∃z.R(x, y , z)
1.2 ∀x.∃z.R(x, f (x), z)
1.3 ∀x.R(x, f (x), g (x))
2. Alternativa 2 (azul, rojo)
2.1 ∀x.∃y .∃z.R(x, y , z)
2.2 ∀x.∃y .R(x, y , h(x, y ))
2.3 ∀x.R(x, k(x), h(x, k(x)))
3. La skolemización no es determinı́stica.
Ejemplos

I Considere la sentencia:
∀x.∃y .∃z.R(x, y , z)
1. Alternativa 1 (rojo, azul)
1.1 ∀x.∃y .∃z.R(x, y , z)
1.2 ∀x.∃z.R(x, f (x), z)
1.3 ∀x.R(x, f (x), g (x))
2. Alternativa 2 (azul, rojo)
2.1 ∀x.∃y .∃z.R(x, y , z)
2.2 ∀x.∃y .R(x, y , h(x, y ))
2.3 ∀x.R(x, k(x), h(x, k(x)))
3. La skolemización no es determinı́stica.
I Es mejor skolemizar de afuera hacia adentro.
Forma clausal

Hasta ahora tenemos una fórmula que:

1. está escrita en términos de ∧, ∨, ¬, ∀;
2. si tiene negaciones, solamente se aplican a átomos (forma
normal negada);
3. si tiene cuantificadores, son universales (forma normal de
Skolem);
4. si está en forma normal prenexa y tiene cuantificadores, éstos
se encuentran todos en el prefijo.

∀x1 . . . ∀xn .B
Forma clausal

∀x1 . . . ∀xn .B

1. Pasar B (la matriz) a forma normal conjuntiva B 0 como si

fuera una fórmula proposicional arrojando
∀x1 . . . ∀xn .B 0
Forma clausal

∀x1 . . . ∀xn .B

1. Pasar B (la matriz) a forma normal conjuntiva B 0 como si

fuera una fórmula proposicional arrojando
∀x1 . . . ∀xn .B 0
2. Distribuir los cuantificadores sobre cada conjunción usando la
fórmula válida ∀x.(A ∧ B) ⇐⇒ ∀x.A ∧ ∀x.B arrojando una
conjunción de cláusulas
∀x1 . . . ∀xn .C1 ∧ . . . ∧ ∀x1 . . . ∀xn .Cm
donde cada Ci es una disyunción de literales
Forma clausal

∀x1 . . . ∀xn .B

1. Pasar B (la matriz) a forma normal conjuntiva B 0 como si

fuera una fórmula proposicional arrojando
∀x1 . . . ∀xn .B 0
2. Distribuir los cuantificadores sobre cada conjunción usando la
fórmula válida ∀x.(A ∧ B) ⇐⇒ ∀x.A ∧ ∀x.B arrojando una
conjunción de cláusulas
∀x1 . . . ∀xn .C1 ∧ . . . ∧ ∀x1 . . . ∀xn .Cm
donde cada Ci es una disyunción de literales
3. Se simplifica escribiendo {C1 , . . . , Cm }.
Ejemplo

∀x.∀z.(P(a) ∨ (Q(g (x)) ∧ (P(g (x), z) ∨ Q(x, f (x))))) ∨ Q(c)

1. Pasamos la matriz a forma normal conjuntiva

∀x.∀z. [P(a) ∨ Q(g (x)) ∨ Q(c)] ∧ [P(a)

∨ P(g (x), z) ∨
Q(x, f (x)) ∨ Q(c)]
Ejemplo

∀x.∀z.(P(a) ∨ (Q(g (x)) ∧ (P(g (x), z) ∨ Q(x, f (x))))) ∨ Q(c)

1. Pasamos la matriz a forma normal conjuntiva

∀x.∀z. [P(a) ∨ Q(g (x)) ∨ Q(c)] ∧ [P(a)

∨ P(g (x), z) ∨
Q(x, f (x)) ∨ Q(c)]
2. Distribuimos los cuantificadores
  
∀x.∀z. P(a) ∨ Q(g (x)) ∨ Q(c) ∧ ∀x.∀z. P(a) ∨ P(g (x), z) ∨
Q(x, f (x)) ∨ Q(c)]
Ejemplo

∀x.∀z.(P(a) ∨ (Q(g (x)) ∧ (P(g (x), z) ∨ Q(x, f (x))))) ∨ Q(c)

1. Pasamos la matriz a forma normal conjuntiva

∀x.∀z. [P(a) ∨ Q(g (x)) ∨ Q(c)] ∧ [P(a)

∨ P(g (x), z) ∨
Q(x, f (x)) ∨ Q(c)]
2. Distribuimos los cuantificadores
  
∀x.∀z. P(a) ∨ Q(g (x)) ∨ Q(c) ∧ ∀x.∀z. P(a) ∨ P(g (x), z) ∨
Q(x, f (x)) ∨ Q(c)]
3. Pasamos a notación de conjuntos
n
{P(a), Q(g (x)), Q(c)},
o
{P(a), P(g (x), z), Q(x, f (x)), Q(c)}
Forma clausal - Resumen

1. Escribir la fórmula en términos de ∧, ∨, ¬, ∀, ∃ (i.e. eliminar

implicación)
2. Pasar a forma normal negada
3. Pasar a forma normal prenexa
4. Pasar a forma normal de Skolem (puede hacerse antes de 3)
5. Pasar la matriz a forma normal conjuntiva
6. Distribuir cuantificadores universales
Nota: todos los pasos preservan validez lógica, salvo la
skolemización (que preserva la satisfactibilidad).
Resolución en lógica proposicional

Para probar que A es una tautologı́a hacemos lo siguiente:

1. Calculamos la forma normal conjuntiva B de ¬A.
2. Pasamos B a forma clausal.
3. Aplicamos el método de resolución.
4. Si hallamos una refutación:
I ¬A es insatisfactible,
I y, por lo tanto, A es una tautologı́a.
5. Si no hallamos ninguna refutación:
I ¬A es satisfactible,
I y, por lo tanto, A no es una tautologı́a.
Resolución en lógica proposicional

I Refutación: secuencia de pasos de resolución que llevan a una

forma clausal conteniendo la cláusula vacı́a.
I Pasos de resolución: aplicaciones de la regla de resolución.
{A1 , . . . , Am , Q} {B1 , . . . , Bn , ¬Q}
{A1 , . . . , Am , B1 , . . . , Bn }
I ¿Podemos aplicar esta regla directamente (asumiendo que los
Ai , Bi , Q son predicados atómicos o sus negaciones)?
Resolución en lógica proposicional

Consideremos la siguiente fórmula:

(∀x.P(x)) ∧ ¬P(a)

I ¿Es satisfactible?
Resolución en lógica proposicional

Consideremos la siguiente fórmula:

(∀x.P(x)) ∧ ¬P(a)

I ¿Es satisfactible? NO.

I Su forma clausal es
Resolución en lógica proposicional

Consideremos la siguiente fórmula:

(∀x.P(x)) ∧ ¬P(a)

I ¿Es satisfactible? NO.

I Su forma clausal es
{{P(x)}, {¬P(a)}}
I ¿Podemos aplicar la regla de resolución?
{A1 , . . . , Am , Q} {B1 , . . . , Bn , ¬Q}
{A1 , . . . , Am , B1 , . . . , Bn }
Resolución en lógica proposicional

Consideremos la siguiente fórmula:

(∀x.P(x)) ∧ ¬P(a)

I ¿Es satisfactible? NO.

I Su forma clausal es
{{P(x)}, {¬P(a)}}
I ¿Podemos aplicar la regla de resolución?
{A1 , . . . , Am , Q} {B1 , . . . , Bn , ¬Q}
{A1 , . . . , Am , B1 , . . . , Bn }
I No. P(x) y P(a) no son idénticos, son ... unificables.
Ahora sı́, la Regla de resolución

{B1 , . . . , Bk , A1 , . . . , Am } {¬D1 , . . . , ¬Dj , C1 , . . . , Cn }

σ({A1 , . . . , Am , C1 , . . . , Cn })

donde σ es el MGU de
. . . .
{B1 = B2 , . . . , Bk−1 = Bk , Bk = D1 , . . . , Dj−1 = Dj }.
I Asumimos que las cláusulas {B1 , . . . , Bk , A1 , . . . , Am } y
{¬D1 , . . . , ¬Dj , C1 , . . . , Cn } no tienen variables en común; en
caso contrario se renombran las variables.
I Observar que σ(B1 ) = . . . = σ(Bk ) = σ(D1 ) = . . . = σ(Dj ).
I La cláusula σ({A1 , . . . , Am , C1 , . . . , Cn }) se llama resolvente
(de {B1 , . . . , Bk , A1 , . . . , Am } y {¬D1 , . . . , ¬Dj , C1 , . . . , Cn }).
Método de resolución

I Las siguientes nociones son análogas al caso proposicional.

I Cláusula vacı́a
I Paso de resolución
I Refutación
I Al igual que en el caso proposicional contamos con el
siguiente resultado.
Teorema de Herbrand-Skolem-Gödel
Cada paso de resolución preserva satisfactibilidad.
Ejemplo

Supongamos que dado A, obtenemos ¬A, lo convertimos a forma

clausal y nos queda: C1 ∧ C2 ∧ C3 donde
I C1 = ∀z1 .∀x.(¬P(z1 , a) ∨ ¬P(z1 , x) ∨ ¬P(x, z1 ))
I C2 = ∀z2 .(P(z2 , f (z2 )) ∨ P(z2 , a))
I C3 = ∀z3 .(P(f (z3 ), z3 ) ∨ P(z3 , a))
Abreviado (sin cuantificadores + notación de conjuntos):

{¬P(z1 , a), ¬P(z1 , x), ¬P(x, z1 )},
{P(z2 , f (z2 )), P(z2 , a)},
{P(f (z3 ), z3 ), P(z3 , a)}
Ejemplo

C1 = {¬P(z1 , a), ¬P(z1 , x), ¬P(x, z1 )},

C2 = {P(z2 , f (z2 )), P(z2 , a)},
C3 = {P(f (z3 ), z3 ), P(z3 , a)}.
Ejemplo

C1 = {¬P(z1 , a), ¬P(z1 , x), ¬P(x, z1 )},

C2 = {P(z2 , f (z2 )), P(z2 , a)},
C3 = {P(f (z3 ), z3 ), P(z3 , a)}.

1. De C1 y C2
Ejemplo

C1 = {¬P(z1 , a), ¬P(z1 , x), ¬P(x, z1 )},

C2 = {P(z2 , f (z2 )), P(z2 , a)},
C3 = {P(f (z3 ), z3 ), P(z3 , a)}.

1. De C1 y C2 con {z1 ← a, x ← a, z2 ← a}:

Ejemplo

C1 = {¬P(z1 , a), ¬P(z1 , x), ¬P(x, z1 )},

C2 = {P(z2 , f (z2 )), P(z2 , a)},
C3 = {P(f (z3 ), z3 ), P(z3 , a)}.

1. De C1 y C2 con {z1 ← a, x ← a, z2 ← a}:

C4 = {P(a, f (a))}
Ejemplo

C1 = {¬P(z1 , a), ¬P(z1 , x), ¬P(x, z1 )},

C2 = {P(z2 , f (z2 )), P(z2 , a)},
C3 = {P(f (z3 ), z3 ), P(z3 , a)}.

1. De C1 y C2 con {z1 ← a, x ← a, z2 ← a}:

C4 = {P(a, f (a))}
2. De C1 y C3
Ejemplo

C1 = {¬P(z1 , a), ¬P(z1 , x), ¬P(x, z1 )},

C2 = {P(z2 , f (z2 )), P(z2 , a)},
C3 = {P(f (z3 ), z3 ), P(z3 , a)}.

1. De C1 y C2 con {z1 ← a, x ← a, z2 ← a}:

C4 = {P(a, f (a))}
2. De C1 y C3 con {z1 ← a, x ← a, z3 ← a}:
Ejemplo

C1 = {¬P(z1 , a), ¬P(z1 , x), ¬P(x, z1 )},

C2 = {P(z2 , f (z2 )), P(z2 , a)},
C3 = {P(f (z3 ), z3 ), P(z3 , a)}.

1. De C1 y C2 con {z1 ← a, x ← a, z2 ← a}:

C4 = {P(a, f (a))}
2. De C1 y C3 con {z1 ← a, x ← a, z3 ← a}:
C5 = {P(f (a), a)}
Ejemplo

C1 = {¬P(z1 , a), ¬P(z1 , x), ¬P(x, z1 )},

C2 = {P(z2 , f (z2 )), P(z2 , a)},
C3 = {P(f (z3 ), z3 ), P(z3 , a)}.

1. De C1 y C2 con {z1 ← a, x ← a, z2 ← a}:

C4 = {P(a, f (a))}
2. De C1 y C3 con {z1 ← a, x ← a, z3 ← a}:
C5 = {P(f (a), a)}
3. De C1 y C5
Ejemplo

C1 = {¬P(z1 , a), ¬P(z1 , x), ¬P(x, z1 )},

C2 = {P(z2 , f (z2 )), P(z2 , a)},
C3 = {P(f (z3 ), z3 ), P(z3 , a)}.

1. De C1 y C2 con {z1 ← a, x ← a, z2 ← a}:

C4 = {P(a, f (a))}
2. De C1 y C3 con {z1 ← a, x ← a, z3 ← a}:
C5 = {P(f (a), a)}
3. De C1 y C5 con {z1 ← f (a), x ← a}:
Ejemplo

C1 = {¬P(z1 , a), ¬P(z1 , x), ¬P(x, z1 )},

C2 = {P(z2 , f (z2 )), P(z2 , a)},
C3 = {P(f (z3 ), z3 ), P(z3 , a)}.

1. De C1 y C2 con {z1 ← a, x ← a, z2 ← a}:

C4 = {P(a, f (a))}
2. De C1 y C3 con {z1 ← a, x ← a, z3 ← a}:
C5 = {P(f (a), a)}
3. De C1 y C5 con {z1 ← f (a), x ← a}:
C6 = {¬P(a, f (a))}
Ejemplo

C1 = {¬P(z1 , a), ¬P(z1 , x), ¬P(x, z1 )},

C2 = {P(z2 , f (z2 )), P(z2 , a)},
C3 = {P(f (z3 ), z3 ), P(z3 , a)}.

1. De C1 y C2 con {z1 ← a, x ← a, z2 ← a}:

C4 = {P(a, f (a))}
2. De C1 y C3 con {z1 ← a, x ← a, z3 ← a}:
C5 = {P(f (a), a)}
3. De C1 y C5 con {z1 ← f (a), x ← a}:
C6 = {¬P(a, f (a))}
4. De C4 y C6 : 2
Diferencias con proposicional

1. En proposicional
{Q, A1 , . . . , Am } {¬Q, B1 , . . . , Bn }
{A1 , . . . , Am , B1 , . . . , Bn }
2. En primer orden
{B1 , . . . , Bk , A1 , . . . , Am } {¬D1 , . . . , ¬Dj , C1 , . . . , Cn }
σ({A1 , . . . , Am , C1 , . . . , Cn })
donde σ es el MGU de {B1 , . . . , Bk , D1 , . . . , Dj }.
Regla de resolución binaria

{B, A1 , . . . , Am } {¬D, C1 , . . . , Cn }
σ({A1 , . . . , Am , C1 , . . . , Cn })

donde σ es el MGU de {B, D}.

I Es incompleta.
I Ejemplo: intentar refutar {{P(x), P(y )}, {¬P(v ), ¬P(w )}}
Regla de resolución binaria

I Se puede recuperar la completitud incorporando una regla

adicional: factorización.
{B1 , . . . , Bk , A1 , . . . , Am }
σ({B1 , A1 , . . . , Am })
donde σ es el MGU de {B1 , . . . , Bk }.
I En el ejemplo anterior
1. {{P(x), P(y )}, {¬P(v ), ¬P(w )}}
2. {{P(x), P(y )}, {¬P(v ), ¬P(w )}, {P(z)}} (fact.)
3. {{P(x), P(y )}, {¬P(v ), ¬P(w )}, {P(z)}, {¬P(u)}} (fact.)
4. {{P(x), P(y )}, {¬P(v ), ¬P(w )}, {P(z)}, {¬P(u)}, 2}
(resolución (binaria))