Logica proposicional

Lógica
Unificación y Resolución con UMG

Departamento de Inteligencia Artificial
Facultad de informática

Curso académico 2012-2013
Pepa Hernández

Sustituciones
n 

n 
n 

n 

Una sustitución es una función finita de un conjunto de variables de un
lenguaje en el de términos. Se representa como α = {x1/t1, x2/t2, …, xn/tn}
donde x1, …, xn son variables diferentes y t1, …,tn son términos.
Un par xi/ti se denomina ligadura
Una sustitución que no sustituye ninguna variable se llama sustitución vacía
(λ)
Una sustitución que sustituye variables por otras variables se denomina
renombrado
Ejemplos: Ctes = {a, b, c, d}, Var = {x, y, z, w}, Func = {f/1, h/2}
q 

α1 = {x/f(a), y/x, z/h(b,y), w/a}

q 

α2 = {x/a, y/a, z/h(b,c), w/f(d)}

q 

α3 = {x/y,z/w} (renombrado)

q 

λ = {x/x, y/y, z/z}

Sustituciones
n 

Dada una sustitución α = {x1/t1, …, xn/tn}, se denomina
aplicación de α a una fórmula F (o a un término t) a la fórmula
obtenida reemplazando simultáneamente cada ocurrencia en F
(o en t) de xi por ti, para cada xi/ti ∈ α.
n 
n 

P(x, y, z) α = P(f(a), f(a), h(b,f(a)))

incorrecto

n 

n 

α = {x/f(a), y/x,z/h(b,y), w/a}
P(x, y, z) α = P(f(a), x, h(b,y))

correcto

Una fórmula F’ es instancia de otra F si existe una sustitución
no vacía α tal que F’ = Fα

Composición de sustituciones
n 

Dadas dos sustituciones α = {x1/t1, …, xn/tn} y β= {y1/s1, …, ym/sm} su
composición αβ se define eliminando del conjunto
{x1/t1β, …, xn/tnβ, y1/s1, …, ym/sm}
q 
q 

n 

las ligaduras xi/tiβtales que xi ≡ tiβ,
y las ligaduras yi/si tales que yi ∈ {x1,…,xn}

Ejemplo: α = {x/3,y/f(x,1)} y β= {x/4}
q 
q 

n 

αβ = {x/3, y/f(4,1)}
βα = {x/4, y/f(x,1)}

Propiedades de la composición:
q 
q 
q 
q 

(Fα)β = F(αβ)
(αβ)γ = α(βγ)
αλ=λα=α
αβ ≠ βα

Unificadores
n 

n 

Una sustitución α es un unificador de dos fórmulas A y B si Aα = Bα. En
este caso se diceque A y B son unificables
Un unificador α de A y B se denomina unificador de máxima generalidad
(umg) sii para cualquier otro unificador β de A y B existe alguna
sustitución γ tal que β=αγ

n 

Si dos fórmulas son unificables entonces tienen umg

n 

El umg de dos fórmulas es único (salvo renombrado)

n 

Ejemplo:
q 

A ≡ P(x, f(x, g(y)), z) y B ≡ P(r, f(r, u), a)

q 

α1= {x/r, u/g(y), z/a} y α2 = {x/a, r/a, y/b, u/g(b), z/a}

q 

Aα1 = Bα1 = P(r, f(r, g(y)), a)

q 

Aα2 = Bα2 = P(a, f(a, g(b)), a)

q 

α1 y α2 son unificadores de A y B, pero α1 es el umg de A y B

q 

γ = {r/a, y/b}, α2 = α1 γ

Algoritmo de Unificación
Sean A y B dos átomos con el mismo símbolo de predicado:
(1) α = λ
(2) Mientras Aα ≠ Bα:
(2.1) Encontrar el símbolomás a la izquierda en Aα tal que el símbolo
correspondiente en Bα sea diferente
(2.2) Sean tA y tB los términos de Aα y Bα que empiezan con esos
símbolos:
(a) Si ni tA ni tB son variables o, si uno de ellos es una variable
que aparece en el otro è terminar con fallo (A y B no son
unificables)
(b) En otro caso, sea tA una variable è el nuevo α es el
resultado de α{tA/tB}
(3) Terminar,siendo α el umg de A y B

Algoritmo de Unificación
n 

Ejemplo: A ≡ P(x, x) y B ≡ P(f(a), f(b))
α

Aα

Bα

(tA, tB)

λ

P(x, x)

P(f(a), f(b))

(x,f(a))

{x/f(a)}

P(f(a), f(a))

P(f(a), f(b))

(a,b)

Fallo è A y B no son unificables
n 

Ejemplo: A ≡ P(x, f(y)) y B ≡ P(z, x)
α

Aα

Bα

(tA, tB)

λ

P(x, f(y))

P(z, x)

(x,z)

{x/z}

P(z, f(y))P(z, z)

(f(y),z)

{x/f(y), z/f(y)} P(f(y), f(y))

P(f(y), f(y))

è A y B son unificables y su umg es {x/f(y), z/f(y)}

Resolución con variables
n 

Regla de resolución con umg: Sean L1 ∨ ... ∨ Ln ∨ C1 y ¬L1’ ∨ ... ∨ ¬Lm’ ∨
C2 dos cláusulas, donde todos los Lij son literales con el mismo símbolo de
predicado. Puede deducirse una nueva cláusula (C1 ρ1 ∨ C2 ρ2)β, llamada...