PDF de programación - Tema 9: Resolución en lógica de primer orden

Resolución de
primer orden

Resolución básica

Resolución no
restringida

Unificación
Ejemplos

Resolución

Paramodulación

Tema 9:

Resolución en lógica de primer orden

Dpto. Ciencias de la Computación Inteligencia Artificial

Universidad de Sevilla

Lógica Informática

(Tecnologías Informáticas)

Curso 2015–16

Resolución de
primer orden

Resolución básica

Resolución no
restringida

Unificación
Ejemplos

Resolución

Paramodulación

Contenido

Resolución básica

Resolución no restringida

Unificación

Ejemplos

Resolución

Paramodulación

Resolución de
primer orden

Resolución básica

Resolución no
restringida

Unificación
Ejemplos

Resolución

Paramodulación

Introducción

Por el Teorema de Herbrand, un conjunto de cláusulas,
Σ, es inconsistente si y sólo si su extensión de Herbrand,
EH(Σ), es inconsistente (proposicionalmente).

Esto proporciona una forma rudimentaria del método de
resolución para probar que un conjunto, Σ, de cláusulas
de un lenguaje de primer orden es inconsistente:
1. Generar EH(Σ) y,
2. Probar que EH(Σ) r .

El método de resolución en lógica de primer orden

incorpora varias mejoras en este procedimiento básico:

1. Es posible generar EH(Σ) poco a poco, calculando sólo
las sustituciones necesarias para obtener cada una de las
cláusulas con las que se calculan la resolventes.

2. No es necesario restringir el cálculo de resolventes

proposicionales a cláusulas sin variables, y

3. Para calcular una resolvente proposicional entre dos

cláusulas, podemos conseguir que ambas cláusulas se
obtengan aplicando la misma sustitución a dos cláusulas
de Σ (y dicha sustitución se obtiene algorítmicamente).

Ejemplo

Sea Σ = {C1, C2, C3} el conjunto de las cláusulas

C1 : ¬P(a, y ) ∨ ¬P(y , z) ∨ ¬P(z, y ),
P(x, f (x)) ∨ P(a, x),
C2
C3 : P(f (x), x) ∨ P(a, x)

siendo a una constante.

Para probar que Σ es inconsistente basta probar que su

extensión de Herbrand EH(Σ) es inconsistente
(proposicionalmente).

Consideremos las siguientes sustituciones:

Resolución de
primer orden

Resolución básica

Resolución no
restringida

Unificación
Ejemplos

Resolución

Paramodulación

θ1 = {y /a, z/a}
θ2 = {y /a, z/f (a)}
θ3 = {y /f (a), z/a}
θ4 = {x/a}

Entonces C1θ1, C1θ2, C1θ3, C2θ4, C3θ4 ∈ EH(Σ).

Ejemplo (II)

Las cláusulas

E1 = C1θ1 : ¬P(a, a)
E2 = C1θ2 : ¬P(a, a) ∨ ¬P(a, f (a)) ∨ ¬P(f (a), a)
E3 = C1θ3 : ¬P(a, f (a)) ∨ ¬P(f (a), a)
E4 = C2θ4 : P(a, f (a)) ∨ P(a, a),
E5 = C3θ4 : P(f (a), a) ∨ P(a, a)

son fórmulas abiertas sin variables.

Veamos que EH(Σ) es inconsistente. Para ello

probamos que S = {E1, E2, E3, E4, E5} ⊆ EH(Σ) es
inconsistente utilizando resolución proposicional:

Resolución de
primer orden

Resolución básica

Resolución no
restringida

Unificación
Ejemplos

Resolución

Paramodulación



E1
E4 → P(a, f (a)) → ¬P(f (a), a) → P(a, a) →



E5



E3



E1

Ejemplo (III)

Cada resolvente proposicional entre cláusulas de EH(Σ)

puede obtenerse directamente a partir de las cláusulas
de Σ si se toma nota de las sustituciones utilizadas para
generar las cláusulas de EH(Σ).

Ejemplo: La resolvente P(a, f (a)) obtenida a partir de
E1 y E4, puede considerarse obtenida a partir de C1 y
C2 utilizando las sustituciones θ1 y θ4.

Gráficamente,

Resolución de
primer orden

Resolución básica

Resolución no
restringida

Unificación
Ejemplos

Resolución

Paramodulación

C1
sustitución θ1 ↓

C2
↓ sustitución θ4

C1θ1



C2θ4



P(a, f (a))

(resolvente proposicional)

Si las sustituciones utilizadas pueden dejar variables

libres obtenemos una resolvente no restringida.

Resolución de
primer orden

Resolución básica

Resolución no
restringida

Unificación
Ejemplos

Resolución

Paramodulación

Resolventes no restringidas

Decimos que C es una resolvente no restringida de

las cláusula C1 y C2 si

C1 = {A1, . . . , An, L1, . . . , Lk}
C2 = {B1, . . . , Bm, M1, . . . , Mr}

y existen dos sustituciones θ1 y θ2 y un literal L tales
que:

{L1, . . . , Lk}θ1 = {L}.
{M1, . . . , Mr}θ2 = {Lc} (literal complementario de L), y
C = {A1θ1, . . . , Anθ1, B1θ2, . . . , Bmθ2}.

Es decir,

C = (C1θ1 \ {L}) ∪ (C2θ2 \ {Lc})

En otra palabras C es una resolvente no restringida de
C1 y C2 si existen dos subcláusulas D1 ⊆ C1 y D2 ⊆ C2
y dos sustituciones θ1 y θ2 y un literal L tales que

D1θ1 = {L} y D2θ2 = {Lc}
C es una resolvente proposicional de C1θ1 y C2θ2 con

respecto al literal L.

Ejemplos

Si las cláusulas son cerradas, una resolvente no

restringida es una resolvente proposicional.

Las resolventes no restringidas no son únicas, incluso

respecto al mismo par de literales:

Resolución de
primer orden

Resolución básica

Resolución no
restringida

Unificación
Ejemplos

Resolución

Paramodulación

{Padre de(x, Ana), Hermano(Ana, x)},

{¬Padre de(y , x), ¬Madre de(y , x)}

↓ θ1 = {x/z}
↓ θ2 = {x/Ana, y /z}
{Hermano(Ana, z), ¬Madre de(z, Ana)}

{Padre de(x, Ana), Hermano(Ana, x)}, {¬Padre de(y , x), ¬Madre de(y , x)}

↓ θ1 = {x/Pedro}
↓ θ2 = {x/Ana, y /Pedro}
{Hermano(Ana, Pedro), ¬Madre de(Pedro, Ana)}

Resolución de
primer orden

Resolución básica

Resolución no
restringida

Unificación
Ejemplos

Resolución

Paramodulación

Demostraciones por resolución

Dado un conjunto de cláusulas, Σ, podemos considerar el
sistema deductivo que tiene a Σ como conjunto de axiomas
y resolución no restringida como única regla de inferencia.
Una demostración por resolución no restringida a
partir de Σ es una sucesión de cláusulas C1, . . . , Cn tal
que para cada i = 1, . . . , n se verifica:

Ci ∈ Σ, o bien
Existen j, k < i tales que Ci es una resolvente no

restringida de Cj y Ck .

Si Cn = diremos que C1, . . . , Cn es una refutación
de Σ.

Una cláusula C es demostrable por resolución no

restringida a partir de Σ si existe una demostración a
partir de Σ, C1, . . . , Cn, tal que Cn = C .
Notación: Σ ur C .

Decimos que Σ es refutable si Σ ur .

Ejemplo

Σ = { ¬P(a, y ) ∨ ¬P(y , z) ∨ ¬P(z, y ),

P(x, f (x)) ∨ P(a, x),
P(f (x), x) ∨ P(a, x)}

Resolución de
primer orden

Resolución básica

Resolución no
restringida

Unificación
Ejemplos

Resolución

Paramodulación

[[Hip.]]

Veamos que Σ ur :
1. ¬P(a, y ) ∨ ¬P(y , z) ∨ ¬P(z, y )
2. P(x, f (x)) ∨ P(a, x)
[[Hip.]]
3. P(a, f (a))
4. ¬P(f (a), a)
5. P(f (x), x) ∨ P(a, x)
6. P(a, a)
7.

[[Hip.]]

[[Res(5,4), θ1 = {x/a}, θ2 = ∅]]
[[Res(1, 6), θ1 = {y /a, z/a}, θ2 = ∅]]

[[Res(1, 2), θ1 = {y /a, z/a}, θ2 = {x/a}]]
[[Res(1, 3), θ1 = {y /f (a), z/a}, θ2 = ∅]]

Otro ejemplo
Σ = {R(x, y ) ∨ R(y , z), ¬R(x, f (x))}
Veamos que Σ ur .
1. R(x, y ) ∨ R(y , z)
2. ¬R(x, f (x))
3. R(f (x), z)
4. [[Res(2, 3), θ1 = {x/f (u)}, θ2 = {x/u, z/f (f (u))}]]

[[Hip.]]
[[Res(1, 2), θ1 = {y /f (x)}, θ2 = ∅]]

[[Hip.]]

Resolución de
primer orden

Resolución básica

Resolución no
restringida

Unificación
Ejemplos

Resolución

Paramodulación

Unificadores

Sea C una cláusula de primer orden y D una subcláusula
de C tal que existe una sustitución θ para la que Dθ se
reduce a un único literal L. Entonces decimos que

La sustitución θ unifica el conjunto de expresiones D.
D es unificable y θ es un unificador de D.

Un problema central del cálculo de resolventes no
restringidas entre dos cláusulas C1 y C2 es encontrar las
subcláusulas D1 ⊆ C1 y D2 ⊆ C2 unificables y los
unificadores θ1 y θ2 que hacen que D1θ1 y D2θ2 se
reduzcan a literales complementarios.

El problema puede reducirse a la búsqueda de una sola

sustitución. Para ello:

Resolución de
primer orden

Resolución básica

Resolución no
restringida

Unificación
Ejemplos

Resolución

Paramodulación

1. Podemos suponer que C1 y C2 no tienen variables
comunes (condición de variables separadas).
2. Buscamos D1 ⊆ C1 y D2 ⊆ C2 tales que D1 ∪ D c

2 (o

bien D c

1 ∪ D2) satisface que:

Es unificable, y
sus literales son positivos y tienen el mismo predicado.
i está formada por los literales complementarios de

(D c
los literales de Di ).

Resolución de
primer orden

Resolución básica

Resolución no
restringida

Unificación
Ejemplos

Resolución

Paramodulación

Unificadores

Si D es un conjunto de literales, una sustitución θ es un

unificador de D si Dθ es unitaria.

Un unificador θ de D es un unificador de máxima

generalidad (u.m.g.) si

Para todo unificador σ de D, existe una sustitución α

tal que σ = θα.
(siendo θα la composición de θ y α, es decir, la
sustitución obtenida al aplicar primero la sustitución θ y
luego α).

Ejemplo de u.m.g. de literales:

θ1 = {y /x, u/Ana, z/Ana} es un u.m.g. de

Padre de(x, z), Padre de(y , Ana), Padre de(x, u)
y θ2 = {x/Ana, y /Ana, u/Ana, z/Ana} es unificador,
pero no es un u.m.g.:

θ2 = {y /x, u/Ana, z/Ana}{x/Ana}

Resolución de
primer orden

Resolución básica

Resolución no
restringida

Unificación
Ejemplos

Resolución

Paramodulación

Algoritmo para obtener un u.m.g.
1, . . . , t

Para unificar pt1, . . . , tn y pt

n, debemos obtener

1θ, . . . , tnθ = t
nθ.

una sustitución θ que sea solución de las ecuaciones:
t1θ = t
n}
1, . . . , tn = t

Para ello aplicamos al conjunto {t1 = t
las siguientes reglas, mientras sea posible:
R1: {x = x} ∪ E =⇒ E
R2: {x = t} ∪ E =⇒ {x = t} ∪ E{x/t}
cuando x ocurre en E y no en t
R3: {t = x} ∪ E =⇒ {x = t} ∪ E
R4: {f (t1, . . . , tn) = f (t
1, . . . , t
R5: {f (t1, . . . , tn) = g (t
1, . . . , t
R6: {x = t} ∪ E =⇒ FALLO
{x1 = s1, x2 = s2, . . . , xr =