Lógica informática Curso 2004–05

Tema 9: Resolución en lógica de

primer orden

José A. Alonso Jiménez

Andrés Cordón Franco

Grupo de Lógica Computacional

Dpto. de Ciencias de la Computación e Inteligencia Artificial

Universidad de Sevilla

LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.1

 Introducción

• Ejemplos de consecuencia mediante resolución:

• Ejemplo 1: {(∀x)[P (x) → Q(x)], (∃x)P (x)} |= (∃x)Q(x)
syss {{¬P (x), Q(x)}, {P (a)}, {¬Q(z)}} es inconsistente.
1 {¬P (x), Q(x)} Hipótesis
2 {P (a)} Hipótesis
3 {¬Q(z)} Hipótesis
4 {Q(a)} Resolvente de 1 y 2 con σ = [x/a]
5 ¤ Resolvente de 3 y 4 con σ = [z/a]
• Ejemplo 2: {(∀x)[P (x) → Q(x)], (∀x)[Q(x) → R(x)]} |= (∀x)[P (x) → R(x)]
syss {{¬P (x), Q(x)}, {¬Q(y), R(y)}, {P (a)}, {¬R(a)}} es inconsistente.
1 {¬P (x), Q(x)} Hipótesis
2 {¬Q(y), R(y)} Hipótesis
3 {P (a)} Hipótesis
4 {¬R(a)} Hipótesis
5 {Q(a)} Resolvente de 1 y 2 con σ = [x/a]
6 {R(a)} Resolvente de 2 y 5 con σ = [y/a]
5 ¤ Resolvente de 3 y 4 con σ = ²
LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.2
 Unificación: Unificadores
• Unificador:
• Def.: La sustitución σ es un unificador de los términos t1 y t2 si t1σ = t2σ.
• Def.: Los términos t1 y t2 son unificables si tienen algún unificador.
• Def.:t es una instancia común de t1 y t2 si existe una sustitución σ tal que t =
t1σ = t2σ.
• Ejemplos:

t1 t2 Unificador Instancia común

f (x, g(z)) f (g(y), x) [x/g(z), y/z] f (g(z), g(z))
f (x, g(z)) f (g(y), x) [x/g(y), z/y] f (g(y), g(y))
f (x, g(z)) f (g(y), x) [x/g(a), y/a] f (g(a), g(a))
f (x, y) f (y, x) [x/a, y/a] f (a, a)
f (x, y) f (y, x) [y/x] f (x, x)
f (x, y) g(a, b) No tiene No tiene
f (x, x) f (a, b) No tiene No tiene
f (x) f (g(x)) No tiene No tiene
• Nota: Las anteriores definiciones se extienden a conjuntos de términos y de literales.

LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.3

 Unificación: Composición de sustituciones

• Composición de sustituciones:
• Def.:La composición de las sustituciones σ1 y σ2 es la sustitución σ1σ2 definida
por x(σ1σ2) = (xσ1)σ2, para toda variable x.
• Ejemplo: Si σ1 = [x/f (z, a), y/w] y σ2 = [x/b, z/g(w)], entonces
– xσ1σ2 = (xσ1)σ2 = f (z, a)σ2 = f (zσ2, aσ2) = f (g(w), a)
– yσ1σ2 = (yσ1)σ2 = wσ2 = w
– zσ1σ2 = (zσ1)σ2 = zσ2 = g(w)
– wσ1σ2 = (wσ1)σ2 = wσ2 = w
Por tanto, σ1σ2 = [x/f (g(w), a), y/w, z/g(w)].
• Def.: La substitución identidad es la sustitución ² tal que, para todo x, x² = x.
• Propiedades:

1. Asociativa: σ1(σ2σ3) = (σ1σ2)σ3

2. Neutro: σ² = ²σ = σ.
LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.4
 Unificación: Comparación de sustituciones

• Comparación de sustituciones:
• Def.:
La sustitución σ1 es más general que la σ2 si existe una sustitución σ3 tal que
σ2 = σ1σ3, Se representa por σ2 ≤ σ1.
• Def.:
Las sustituciones σ1 y σ2 son equivalentes si σ1 ≤ σ2 y σ2 ≤ σ1. Se representa
por σ1 ≡ σ2.
• Ejemplos: Sean σ1 = [x/g(z), y/z], σ2 = [x/g(y), z/y] y σ3 = [x/g(a), y/a]. En-
tonces,
1. σ1 = σ2[y/z]
2. σ2 = σ1[z/y]
3. σ3 = σ1[z/a]
4. σ1 ≡ σ2
5. σ3 ≤ σ1

• Ejemplo: [x/a, y/a] ≤ [y/x], ya que [x/a, y/a] = [y/x][x/a, y/a].

LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.5

 Unificación: Unificador de máxima generalidad

• Unificador de máxima generalidad:

• Def.: La sustitución σ es un unificador de máxima generalidad (UMG) de los
términos t1 y t2 si
– σ es un unificador de t1 y t2.
– σ es más general que cualquier unificador de t1 y t2.

• Ejemplos:

1. [x/g(z), y/z] es un UMG de f (x, g(z)) y f (g(y), x).

2. [x/g(y), z/y] es un UMG de f (x, g(z)) y f (g(y), x).
3. [x/g(a), y/a] no es un UMG de f (x, g(z)) y f (g(y), x).

• Nota: Las anterior definición se extienden a conjuntos de términos y de literales.

LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.6

 Unificación: Algoritmo de unificación
• Notación de lista:
• (a , . . . , a ) representa una lista cuyos elementos son a1, . . . , an.
1 n
• (a|R) representa una lista cuyo primer elemento es a y resto es R.
• () representa la lista vacı́a.

• Unificadores de listas de términos:

• Def.: σ es un unificador de (s1 . . . , sn) y (t1 . . . , tn) si s1σ = t1σ, . . . , snσ = tnσ.
• Def.: (s . . . , s ) y (t . . . , t ) son unificables si tienen algún unificador.
1 n 1 n
• Def.: σ es un unificador de máxima generalidad (UMG) de (s . . . , s ) y (t . . . , t )
1 n 1 n
si σ es un unificador de (s1 . . . , sn) y (t1 . . . , tn) más general que cualquier otro.

• Aplicación de una sustitución a una lista de ecuaciones:

• (s = t1, . . . , sn = tn)σ = (s1σ = t1σ, . . . , snσ = tnσ).
1

• Algoritmo de unificación de listas de términos:

• Entrada: Una lista de ecuaciones L = (s1 = t1, . . . , sn = tn) y una sustitución σ.
• Salida: Un UMG de las listas (s . . . , s ) y (t . . . , t ), si son unificables;
1 n 1 n
“No unificables”, en caso contrario.

LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.7

 Unificación: Algoritmo de unificación

• Procedimiento unif(L, σ):

1. Si L = (), entonces unif(L, σ) = σ.
2. Si L = (t = t|L0), entonces unif(L, σ) = unif(L0, σ).
3. Si L = (f (t1, . . . , tm) = f (t01 . . . , t0m)|L0), entonces
unif(L, σ) = unif((t1 = t01, . . . , tm = t0m|L0), σ).
4. Si L = (x = t|L0) (ó L = (t = x|L0)) y x no aparece en t, entonces
unif(L, σ) = unif(L0[x/t], σ[x/t]).
5. Si L = (x = t|L0) (ó L = (t = x|L0)) y x aparece en t, entonces
unif(L, σ) = “No unificables”.
6. Si L = (f (t1, . . . , tm) = g(t01 . . . , t0m)|L0), entonces
unif(L, σ) = “No unificables”.
7. Si L = (f (t1, . . . , tm) = f (t01 . . . , t0p)|L0) y m 6= p, entonces
unif(L, σ) = “No unificables”.

LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.8

 Unificación: Algoritmo de unificación

• Algoritmo de unificación de dos términos:

• Entrada: Dos términos t1 y t2.
• Salida: Un UMG de t1 y t2, si son unificables;
“No unificables”, en caso contrario.
• Procedimiento: unif((t1 = t2), ²).
• Ejemplo 1: Unificar f (x, g(z)) y f (g(y), x):
unif((f (x, g(z)) = f (g(y), x)), ²)
= unif((x = g(y), g(z) = x), ²) por 3
= unif((g(z) = x)[x/g(y)], ²[x/g(y)]) por 4
= unif((g(z) = g(y)), [x/g(y)])
= unif((z = y), [x/g(y)]) por 3
= unif((), [x/g(y)][z/y]) por 4
= unif((), [x/g(y), z/y])
= [x/g(y), z/y] por 1

LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.9

 Unificación: Algoritmo de unificación
• Ejemplo 2: Unificar f (x, b) y f (a, y):
unif((f (x, b) = f (a, y), ²)
= unif((x = a, b = y), ²) por 3
= unif((b = y)[x/a], ²[x/a]) por 4
= unif((b = y), [x/a])
= unif((), [x/a][y/b]) por 4
= [x/a, y/b]) por 1
• Ejemplo 3: Unificar f (x, x) y f (a, b):
unif((f (x, x) = f (a, b)), ²)
= unif((x = a, x = b), ²) por 3
= unif((x = b)[x/a], ²[x/a]) por 4
= unif((a = b), [x/a])
= “No unificable” por 6
• Ejemplo 4: Unificar f (x, g(y)) y f (y, x):
unif((f (x, g(y)) = f (y, x)), ²)
= unif((x = y, g(y) = x), ²) por 3
= unif((g(y) = x)[x/y], ²[x/y]) por 4
= unif((g(y) = y), [x/y])
= “No unificable” por 5
LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.10
 Unificación: Algoritmo de unificación

• Ejemplo 5: Unificar j(w, a, h(w)) y j(f (x, y), x, z)

unif((j(w, a, h(w)) = j(f (x, y), x, z))²)
= unif((w = f (x, y), a = x, h(w) = z), ²) por 3
= unif((a = x, h(w) = z)[w/f (x, y)], ²[w/f (x, y)]) por 4
= unif((a = x, h(f (x, y)) = z), [w/f (x, y)])
= unif((h(f (x, y)) = z)[x/a], [w/f (x, y)][x/a]) por 4
= unif((h(f (a, y)) = z), [w/f (a, y), x/a])
= unif((), [w/f (a, y), x/a][z/h(f (a, y))]) por 4
= [w/f (a, y), x/a, z/h(f (a, y))) por 1
• Ejemplo 6: Unificar j(w, a, h(w)) y j(f (x, y), x, y)
unif((j(w, a, h(w)) = j(f (x, y), x, y))²)
= unif((w = f (x, y), a = x, h(w) = y), ²) por 3
= unif((a = x, h(w) = y)[w/f (x, y)], ²[w/f (x, y)]) por 4
= unif((a = x, h(f (x, y)) = y), [w/f (x, y)])
= unif((h(f (x, y)) = y)[x/a], [w/f (x, y)][x/a]) por 4
= unif((h(f (a, y)) = y), [w/f (a, y), x/a])
= “No unificable” por 5
LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.11
 Resolución: Separación de variables

• Separación de variables
• Def.:La sustitución [x1/t1, . . . , xn/tn] es un renombramiento si todos los ti son
variables.
• Prop.: Si θ es un renombramiento, entonces C ≡ Cθ.
• Def.: Las cláusulas C1 y C2 están separadas sin no tienen ninguna variable común.
• Def.: Una separación de las variables de C1 y C2 es un par de renombramientos
(θ1, θ2) tales que C1θ1 y C2θ2 están separadas.
• Ejemplo: Una separación de variables de C1 = {P (x), Q(x, y)} y C2 = {R(f (x, y))}
es (θ1 = [x/x1, y/y1], θ2 = [x/x2, y/y2]).

LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.12

 Resolución: Resolvente binaria

• Resolución binaria:
• Def.:
La cláusula C es una resolvente binaria de las cláusulas C1 y C2 si existen una
separación de variables (θ1, θ2) de C1 y C2, un literal L1 ∈ C1, un literal L2 ∈ C2 y
un UMG σ de L1θ1 y Lc2θ2 tales que
C = (C1θ1σ r {L1θ1σ1}) ∪ (C2θ2σ r {L2θ2σ}).
• Ejemplo: Sean
C1 = {¬P (x), Q(f (x))},
C2 = {¬Q(x), R(g(x))},
L1 = Q(f (x)),
L2 = ¬Q(x),
θ1 = [x/x1],
θ2 = [x/x2],
L1θ1 = Q(f (x1)),
Lc2θ2 = Q(x2),
σ = [x2/f (x1)]
Entonces, C = {¬P (x1), R(g(f (x1)))} es una resolvente binaria de C1 y C2.

LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.13

 Resolución: Factorización

• Factorización:
• Def.:
La cláusula C es un factor de la cláusula D si existen dos literales L1 y L2 en
D que son unificables y C = Dσ r {L2σ} donde σ es un UMG de L1 y L2.
• Ejemplo: Sean
D = {P (x, y), P (y, x), Q(a)}
L1 = P (x, y)
L2 = P (y, x)
σ = [y/x]
Entonces,
C = {P (x, x), Q(a)} es un factor de D.

LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.14

 Resolución
• Ejemplos de refutación por resolución:
• Refutación de S = {{¬P (x, f (x, y))}, {P (a, z), ¬Q(z, v)}, {Q(u, a)}}
1 {¬P (x, f (x, y))} Hipótesis
2 {P (a, z), ¬Q(z, v)} Hipótesis
3 {Q(u, a)} Hipótesis
4 {¬Q(f (a, y), v)} Resolvente de 1 y 2 con σ = [x/a, z/f (a, y)]
5 ¤ Resolvente de 3 y 4 con σ = [u/f (a, y), v/a]
• Refutación de S = {{P (x)}, {¬P (f (x))}}
1 {P (x)} Hipótesis
2 {¬P (f (x))} Hipótesis
3 ¤ Resolvente de 1 y 2 con θ1 = ², θ2 = [x/x0], σ = [x/f (x0)]
• Refutación de S = {{P (x, y), P (y, x)}, {¬P (u, v), ¬P (v, u)}}
1 {P (x, y), P (y, x)} Hipótesis
2 {¬P (u, v), ¬P (v, u)} Hipótesis
3 {P (x, x)} Factor de 1 con [y/x]
4 {¬P (u, u)} Factor de 2 con [v/u]
5 ¤ Resolvente de 3 y 4 con [x/u]

LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.15

 Resolución

• Definiciones
• Sea S un conjunto de cláusulas.
• Lasucesión (C1, . . . , Cn) es una demostración por resolución de la cláusula C a
partir de S si C = Cn y para todo i ∈ {1, ..., n} se verifica una de las siguientes
condiciones:
– Ci ∈ S;
– existen j, k < i tales que Ci es una resolvente de Cj y Ck
– existe j < i tal que Ci es un factor de Cj

• Lacláusula C es demostrable por resolución a partir de S si existe una demostración

por resolución de C a partir de S.
• Una refutación por resolución de S es una demostración por resolución de la cláusula
vacı́a a partir de S.
• Sedice que S es refutable por resolución si existe una refutación por resolución a
partir de S.

LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.16

 Resolución

• Demostraciones por resolución

• Def.:Sean S1, . . . , Sn formas clausales de las fórmulas F1, . . . , Fn y S una forma
clausal de ¬F . Una demostración por resolución de F a partir de {F1, . . . , Fn} es
una refutación por resolución de S1 ∪ . . . ∪ Sn ∪ S.
• Def.:La fórmula F es demostrable por resolución a partir de {F1, . . . , Fn} si existe
una demostración por resolución de F a partir de {F1, . . . , Fn}.
Se representa por {F1, . . . , Fn} `Res F .
• Ejemplo: (tema 8 p. 21) {(∀x)[P (x) → Q(x)], (∃x)P (x)} `Res (∃x)Q(x)
1 {¬P (x), Q(x)} Hipótesis
2 {P (a)} Hipótesis
3 {¬Q(z)} Hipótesis
4 {Q(a)} Resolvente de 1 y 2 con [x/a]
5 ¤ Resolvente de 3 y 4 con [z/a]

LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.17

 Resolución
• Ejemplo: (tema 8 p. 21)
{(∀x)[P (x) → Q(x)], (∀x)[Q(x) → R(x)] `Res (∀x)[P (x) → R(x)]}
1 {¬P (x), Q(x)} Hipótesis
2 {¬Q(y), R(y)} Hipótesis
3 {P (a)} Hipótesis
4 {¬R(a)} Hipótesis
5 {Q(a)} Resolvente de 1 y 2 con [x/a]
6 {R(a)} Resolvente de 2 y 5 con [y/a]
5 ¤ Resolvente de 6 y 4 con
• Ejemplo: (tema 6 p. 55) `Res (∃x)[P (x) → (∀y)P (y)]
1 {P (x)} Hipótesis
2 {¬P (f (x))} Hipótesis
3 ¤ Resolvente de 1 y 2 con θ2 = [x/x0], σ = [x/f (x0)]

LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.18

 Resolución
• Ejemplo: `Res (∀x)(∃y)¬(P (y, x) ↔ ¬P (y, y))
– Forma clausal:
¬(∀x)(∃y)¬(P (y, x) ↔ ¬P (y, y))
≡ ¬(∀x)(∃y)¬((P (y, x) → ¬P (y, y)) ∧ (¬P (y, y) → P (y, x)))
≡ ¬(∀x)(∃y)¬((¬P (y, x) ∨ ¬P (y, y)) ∧ (¬¬P (y, y) ∨ P (y, x)))
≡ ¬(∀x)(∃y)¬((¬P (y, x) ∨ ¬P (y, y)) ∧ (P (y, y) ∨ P (y, x)))
≡ (∃x)(∀y)¬¬((¬P (y, x) ∨ ¬P (y, y)) ∧ (P (y, y) ∨ P (y, x)))
≡ (∃x)(∀y)((¬P (y, x) ∨ ¬P (y, y)) ∧ (P (y, y) ∨ P (y, x)))
≡sat (∀y)((¬P (y, a) ∨ ¬P (y, y)) ∧ (P (y, y) ∨ P (y, a)))
≡ {{¬P (y, a), ¬P (y, y)}, {P (y, y), P (y, a)}}
– Refutación:
1 {¬P (y, a), ¬P (y, y)} Hipótesis
2 {P (y, y), P (y, a)} Hipótesis
3 {¬P (a, a)} Factor de 1 con [y/a]
4 {¬P (a, a)} Factor de 2 con [y/a]
5 ¤ Resolvente de 3 y 4

LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.19

 Resolución
• Ejemplo (Paradoja del barbero de Russell): En una isla pequeña hay sólo un bar-
bero. El gobernador de la isla ha publicado la siguiente norma: “El barbero afeita
a todas las personas que no se afeitan a sı́ misma y sólo a dichas personas”. De-
mostrar que la norma es inconsistente.
– Representación:
(∀x)[afeita(b, x) ↔ ¬afeita(x, x)]
– Forma clausal:
(∀x)[afeita(b, x) ↔ ¬afeita(x, x)]
≡ (∀x)[(afeita(b, x) → ¬afeita(x, x)) ∧ (¬afeita(x, x) → afeita(b, x))]
≡ (∀x)[(¬afeita(b, x) ∨ ¬afeita(x, x)) ∧ (¬¬afeita(x, x) ∨ afeita(b, x))]
≡ (∀x)[(¬afeita(b, x) ∨ ¬afeita(x, x)) ∧ (afeita(x, x) ∨ afeita(b, x))]
≡ {{¬afeita(b, x), ¬afeita(x, x)}, {afeita(x, x), afeita(b, x)}}
– Refutación:
1 {¬afeita(b, x), ¬afeita(x, x)} Hipótesis
2 {afeita(x, x), afeita(b, x)} Hipótesis
3 {¬afeita(b, b)} Factor de 1 con [x/b]
4 {afeita(b, b)} Factor de 2 con [x/b]
5 ¤ Resolvente de 3 y 4
LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.20
 Adecuación y completitud de la resolución

• Propiedades:
• Si C es una resolvente de C1 y C2, entonces {C1, C2} |= C.
• Si D es un factor de C entonces C |= D.
• Si ¤ ∈ S, entonces S es inconsistente.
• Si el conjunto de cláusulas S es refutable por resolución, entonces S es inconsistente.
• Teor.:
El cálculo de resolución (para la lógica de primer orden sin igualdad) es
adecuado y completo; es decir,
Adecuado: S `Res F =⇒ S |= F
Completo: S |= F =⇒ S `Res F

LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.21

 Interpretaciones de Herbrand

• Def.:El universo de Herbrand de L es el conjunto de los términos básicos de L. Se

representa por UH(L).
• Def.: Una interpretación I = (U, I) de L es una intepretación de Herbrand si
– U es el universo de Herbrand de L;
– I(c) = c, para cada constante c de L;
– I(f ) = f , para cada sı́mbolo de función f de L.

• Def.:La base de Herbrand de L es el conjunto de los átomos básicos de L. Se

representa por BH(L).
• Prop.: Una interpretación de Herbrand queda determinada por un subconjunto de
la base de Herbrand, el conjunto de átomos básicos verdaderos en esa interpretación.
• Ejemplo:Si C = {a, b, c}, F = ∅ y R = {P/1}, entonces las interpretaciones de
Herbrand de L son
n 1 2 3 4 5 6 7 8
In (P ) ∅ {c} {b} {b, c} {a} {a, c} {a, b} {a, b, c}
IHn ∅ {P (c)} {P (b)} {P (b), P (c)} {P (a)} {P (a), P (c)} {P (a), P (b)} {P (a), P (b), P (c)}

LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.22

 Modelos de Herbrand

• Modelos de Herbrand:
• Nota: Las definiciones de universo de Herbrand, base de Herbrand e interpretación
de Herbrand definidas para un lenguaje se extienden a fórmulas y conjuntos de
fórmulas considerando el lenguaje formado por los sı́mbolos no lógicos que aparecen.
• Def.:
Un modelo de Herbrand de una fórmula F es una interpretación de Herbrand
de F que es modelo de F .
• Def.:
Un modelo de Herbrand de un conjunto de fórmulas S es una interpretación
de Herbrand de S que es modelo de S.
• Ejemplo: Los modelos de Herbrand de {P (a) ∨ P (b), ¬P (b) ∨ P (c), P (a) → P (c)}
son {P (b), P (c)}, {P (a), P (c)} y {P (a), P (b), P (c)}.
• Ejemplo:Sea S = {(∀x)(∀y)[Q(b, x) → P (a) ∨ R(y)], P (b) → ¬(∃z)(∃u)Q(z, u)}.
Entonces, UH(S) = {a, b}
BH(S) = {P (a), P (b), Q(a, a), Q(a, b), Q(b.a), Q(b, b), R(a), R(b)}
Un modelo de Herbrand de S es {P (a)}.

LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.23

 Cálculo de modelo de Herbrand

• Cálculo de modelo de Herbrand

• Ejemplo 1: Cálculo de modelo de Herbrand de {(∀x)[P (x) → Q(x)], P (a), ¬Q(b)}
1 {¬P (x), Q(x)} Hipótesis
2 {P (a)} Hipótesis
3 {¬Q(b)} Hipótesis
4 {Q(a)} Resolvente de 1 y 2
5 {¬P (b)} Resolvente de 1 y 3
Modelo de Herbrand: U = {a, b}, I(P ) = {a}, I(Q) = {a}.
• Ejemplo 2: Cálculo de modelo de Herbrand de {(∀x)[P (x) → P (s(x))], P (0)}
1 {¬P (x), P (s(x))} Hipótesis
2 {P (0)} Hipótesis
3 {P (s(0))} Resolvente de 1 y 2
4 {P (s(s(0)))} Resolvente de 1 y 3
... ... ...

Modelo de Herbrand: U = {0, s(0), s(s(0)), . . .}

I(P ) = {P (0), P (s(0)), P (s(s(0))), . . . , }
LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.24
 Determinación de no–consecuencia por resolución

• Ejemplo de determinación de no consecuencia por resolución

• Enunciado: Comprobar, por resolución, que
(∀x)[P (x) ∨ Q(x)] 6|= (∀x)P (x) ∨ (∀x)Q(x).
• Reducción 1: Comprobar que es consistente
{(∀x)[P (x) ∨ Q(x)], ¬((∀x)P (x) ∨ (∀x)Q(x))}
• Reducción 2: Comprobar que es consistente
{{P (x), Q(x)}, {¬P (a)}, {¬Q(b)}}
• Resolución:

1 {P (x), Q(x)} Hipótesis

2 {¬P (a)} Hipótesis
3 {¬Q(b)} Hipótesis
4 {Q(a)} Resolvente de 1 y 2
5 {P (b)} Resolvente de 1 y 3
• Modelo: U = {a, b}, I(P ) = {b}, I(Q) = {a}.

LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.25

 Tableros semánticos

• Fórmulas gamma y beta

• Las fórmulas gamma, junto con sus componentes, son
(∀x)F F [x/t] (con t un término básico)
¬(∃x)F ¬F [x/t] (con t un término básico)
• Las fórmulas beta, junto con sus componentes, son
(∃x)F F [x/a] (con a una nueva constante)
¬(∀x)F ¬F [x/a] (con a una nueva constante)

LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.26

 Tableros semánticos
• Ejemplo de consecuencia mediante tablero:
{(∀x)[P (x) → Q(x)], (∃x)P (x)} `T ab (∃x)Q(x)

1 (∀x)[P (x) → Q(x)]

2 (∃x)P (x)
3 ¬(∃x)Q(x)
4 P (a) (2)
5 P (a) → Q(a) (1)

6 ¬P (a) (5) 7 Q(a) (5)

Cerrada 8 ¬Q(a) (3)
(6 y 4) Cerrada
(7 y 8)

LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.27

 Tableros semánticos
• Ejemplo de consecuencia mediante tablero:
{(∀x)[P (x) → Q(x)], (∀x)[Q(x) → R(x)]} `T ab (∀x)[P (x) → R(x)]
1 (∀x)[P (x) → Q(x)]
2 (∀x)[Q(x) → R(x)]
3 ¬(∀x)[P (x) → R(x)]
4 ¬(P (a) → R(a)) (3)
5 P (a) (4)
6 ¬R(a) (4)
7 P (a) → Q(a) (1)
8 Q(a) → R(a) (2)

9 ¬P (a) (7) 10 Q(a) (7)

Cerrada
(5 y 9) 11 ¬Q(a) (8) 12 R(a) (8)
Cerrada Cerrada
(10 y 11) (6 y 12)

LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.28

 Tableros semánticos
• Ejemplo de no consecuencia mediante tablero:
(∀x)[P (x) ∨ Q(x)] 6|= (∀x)P (x) ∨ (∀x)Q(x).
1 (∀x)[P (x) ∨ Q(x)]
2 ¬((∀x)P (x) ∨ (∀x)Q(x))
3 ¬(∀x)P (x) (2)
4 ¬(∀x)Q(x) (2)
5 ¬P (a) (3)
6 ¬Q(b) (4)
7 P (a) ∨ Q(a) (1)
8 P (b) ∨ Q(b) (1)

9 P (a) (6) 10 Q(a) (7)

Cerrada
(5 y 9)
11 P (b) (8) 12 Q(b) (8)
Abierta Cerrada
(6 y 12)
Contramodelo: U = {a, b}, I(P ) = {b}, I(Q) = {a}.
LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.29
 Bibliografı́a

• Fitting,M. First-Order Logic and Automated Theorem Proving (2nd ed.)

(Springer, 1996) pp. 137–141.
• M.L. Bonet Apuntes de LPO. (Univ. Politécnica de Cataluña, 2003) pp. 34–40.
• C.L.
Chang y R.C.T. Lee Symbolic logic and mechanical theorem proving (Aca-
demic Press, 1973) pp. 70–99.
• J.I.
Garcı́a, P.A. Garcı́a y J.M. Urbano Fundamentos lógicos de la programación.
(Universidad de Granada, 2002) pp. 45–66
• M.Genesereth Computational Logic (Chapter 9: Relational Resolution) (Stanford
University, 2003)
• S. Hölldobler Computational logic. (U. de Dresden, 2004) pp. 71–74.
• M. Ojeda e I. Pérez Lógica para la computación (Vol. 2: Lógica de Primer Orden)
(Ágora, 1997) pp. 138–164.
• L. Paulson Logic and proof (U. Cambridge, 2002) pp. 50–61.
• U. Schöning Logic for computer scientists (Birkäuser, 1989) pp. 79–96.

LI 2004–05 Cc Ia Resolución en lógica de primer orden 9.30