PDF de programación - Lógica informática (2014–15) - Tema 12: Resolución en lógica de primer orden

PD Tema 12: Resolución en lógica de primer orden

Lógica informática (2014–15)

Tema 12: Resolución en lógica de primer orden

José A. Alonso Jiménez
Andrés Cordón Franco
María J. Hidalgo Doblado

Grupo de Lógica Computacional

Departamento de Ciencias de la Computación e I.A.

Universidad de Sevilla

1 / 31

PD Tema 12: Resolución en lógica de primer orden

Tema 12: Resolución en lógica de primer orden

1. Introducción

2. Unificación

3. Resolución de primer orden

2 / 31

PD Tema 12: Resolución en lógica de primer orden

Introducción

Tema 12: Resolución en lógica de primer orden

1. Introducción

Ejemplos de consecuencia mediante resolución

2. Unificación

3. Resolución de primer orden

3 / 31

PD Tema 12: Resolución en lógica de primer orden

Introducción

Ejemplos de consecuencia mediante resolución

Ejemplos de consecuencia mediante resolución

Ejemplo 1:

se reduce a

{∀x [P(x ) → Q(x )],∃x P(x )} |= ∃x Q(x )
{{¬P(x ), Q(x )},{P(a)},{¬Q(z)}} es inconsistente.

Demostración:
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]

4 / 31

PD Tema 12: Resolución en lógica de primer orden

Introducción

Ejemplos de consecuencia mediante resolución

Ejemplos de consecuencia mediante resolución

Ejemplo 2:

se reduce a

{∀x [P(x ) → Q(x )],∀x [Q(x ) → R(x )]} |= ∀x [P(x ) → R(x )]
{{¬P(x ), Q(x )},{¬Q(y ), R(y )},{P(a)},{¬R(a)}}
es inconsistente.

Demostración:

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 3 con σ = [x /a]
6 {R(a)}
Resolvente de 2 y 5 con σ = [y /a]
5
Resolvente de 4 y 6 con σ =


5 / 31

PD Tema 12: Resolución en lógica de primer orden

Unificación

Tema 12: Resolución en lógica de primer orden

1. Introducción

2. Unificación

Unificadores
Composición de sustituciones
Comparación de sustituciones
Unificador de máxima generalidad
Algoritmo de unificación

3. Resolución de primer orden

6 / 31

PD Tema 12: Resolución en lógica de primer orden

Unificación

Unificadores

Unificadores

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
f (x , g(z))
f (x , g(z))
f (x , g(z))
f (x , y )
f (x , y )
f (x , y )
f (x , x )
f (x )

t2
f (g(y ), x )
f (g(y ), x )
f (g(y ), x )
f (y , x )
f (y , x )
g(a, b)
f (a, b)
f (g(x ))

términos y de literales.

Unificador
[x /g(z), y /z]
[x /g(y ), z/y ]
[x /g(a), y /a]
[x /a, y /a]
[y /x ]
No tiene
No tiene
No tiene

Instancia común
f (g(z), g(z))
f (g(y ), g(y ))
f (g(a), g(a))
f (a, a)
f (x , x )
No tiene
No tiene
No tiene

Nota: Las anteriores definiciones se extienden a conjuntos de

7 / 31

PD Tema 12: Resolución en lógica de primer orden

Unificación

Composición de sustituciones

Composición de sustituciones e identidad

Composición de sustituciones:

Def.: La composición de las sustituciones σ1 y σ2 es la sustitución
Ejemplo: Si σ1 = [x /f (z, a), y /w ] y σ2 = [x /b, z/g(w )], entonces

σ1σ2 definida por x (σ1σ2) = (x σ1)σ2, para toda variable x.

– 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: σ
=
σ = σ.

8 / 31

PD Tema 12: Resolución en lógica de primer orden

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.
σ3 = [x /g(a), y /a]. Entonces,

Ejemplos: Sean σ1 = [x /g(z), y /z], σ2 = [x /g(y ), z/y ] y

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].

9 / 31

PD Tema 12: Resolución en lógica de primer orden

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.

10 / 31

PD Tema 12: Resolución en lógica de primer orden

Unificación

Algoritmo de unificación

Unificación de listas de términos

Notación de lista:

(a1, . . . , an) representa una lista cuyos elementos son a1, . . . , an.
(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.: (s1 . . . , sn) y (t1 . . . , tn) son unificables si tienen algún

unificador.

Def.: σ es un unificador de máxima generalidad (UMG) de

(s1 . . . , sn) y (t1 . . . , tn) 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:

(s1 = t1, . . . , sn = tn)σ = (s1σ = t1σ, . . . , snσ = tnσ).

11 / 31

PD Tema 12: Resolución en lógica de primer orden

Unificación

Algoritmo de unificación

Algoritmo de unificación de listas de términos

Entrada: Lista de ecuaciones L = (s1 = t1, . . . , sn = tn) y

sustitución σ.

Salida:

Un UMG de las listas (s1 . . . , sn)σ y (t1 . . . , tn)σ, si son unificables;
“No unificables”, en caso contrario.

12 / 31

PD Tema 12: Resolución en lógica de primer orden

Unificación

Algoritmo de unificación

Algoritmo de unificación de listas de términos

Procedimiento unif(L, σ):

1. Si L = (), entonces unif(L, σ) = σ.
2. Si L = (t = t|L0), entonces unif(L, σ) = unif(L0, σ).
m)|L0), entonces
1 . . . , t0
3. Si L = (f (t1, . . . , tm) = f (t0
m|L0), σ).
1, . . . , tm = t0
unif(L, σ) = unif((t1 = t0
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
6. Si L = (f (t1, . . . , tm) = g(t0
7. Si L = (f (t1, . . . , tm) = f (t0

unif(L, σ) = “No unificables”.
1 . . . , t0
unif(L, σ) = “No unificables”.
1 . . . , t0
unif(L, σ) = “No unificables”.

m)|L0), entonces
p)|L0) y m 6= p, entonces

13 / 31

PD Tema 12: Resolución en lógica de primer orden

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 )])
= unif((), [x /g(y )][z/y ])
= unif((), [x /g(y ), z/y ])
= [x /g(y ), z/y ]

por 3
por 4

por 1

14 / 31

PD Tema 12: Resolución en lógica de primer orden

Unificación

Algoritmo de unificación

Ejemplos 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 ),
)
= unif((b = y )[x /a],
[x /a])
= unif((b = y ), [x /a])
= unif((), [x /a][y /b])
= [x /a, y /b])

Ejemplo 3: Unificar f (x , x ) y f (a, b):

unif((f (x , x ) = f (a, b)),
)

= unif((x = a, x = b),
)
= unif((x = b)[x /a],
[x /a])
= unif((a = b), [x /a])
= “No unificable”

por 3
por 4

por 4
por 1

por 3
por 4

por 6

15 / 31

PD Tema 12: Resolución en lógica de primer orden

Unificación

Algoritmo de unificación

Ejemplos de unificación

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 ),
)
= unif((g(y ) = x )[x /y ],
[x /y ])
= unif((g(y ) = y ), [x /y ])
= “No unificable”

por 3
por 4

por 5
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),
)
= unif((a = x , h(w ) = z)[w /f (x , y )],
[w /f (x , y )])
= 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])
= unif((h(f (a, y )) = z), [w /f (a, y ), x /a])
= unif((), [w /f (a, y ), x /a][z/h(f (a, y ))])
= [w /f (a, y ), x /a, z/h(f (a, y ))]

por 3
por 4

por 4

por 4
por 116 / 31

PD Tema 12: Resolución en lógica de primer orden

Unificación

Algoritmo de unificación

Ejemplos de unificación

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 ),
)
= unif((a = x , h(w ) = y )[w /f (x , y )],
[w /f (x , y )])
= 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])
= unif((h(f (a, y )) = y ), [w /f (a, y ), x /a])
= “No unificable”

Ejemplo 7: Unificar f (a, y ) y f (a, b):

unif((f (a, y ) = f (a, b),
))

= unif((a = a, y = b),
)
= unif((y = b),
)
= unif((), [y /b])
= [y /b]

por 3
por 2
por 4
por 1

por 3
por 4

por 4

por 5

17 / 31

PD Tema 12: Resolución en lógica de primer orden

Resolución de pri