PDF de programación - Tema 12: Resolución en lógica de primer orden - Lógica matemática y fundamentos (2016–17)

Tema 12: Resolución en lógica de primer orden - Lógica matemática y fundamentos (2016–17)gráfica de visualizaciones

Publicado el 6 de Agosto del 2017
1.240 visualizaciones desde el 6 de Agosto del 2017
225,0 KB
31 paginas
Creado hace 3a (06/02/2017)
LMF Tema 12: Resolución en lógica de primer orden

Lógica matemática y fundamentos (2016–17)

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

José A. Alonso Jiménez
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

LMF 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

LMF 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

LMF 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

LMF 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

LMF 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

LMF 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))

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

términos y de literales.

7 / 31

LMF 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

LMF 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

LMF 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

LMF 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

LMF 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

LMF 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

LMF 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

LMF 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

LMF 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

LMF 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

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

Resolución 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
Separación de
  • Links de descarga
http://lwp-l.com/pdf6140

Comentarios de: Tema 12: Resolución en lógica de primer orden - Lógica matemática y fundamentos (2016–17) (0)


No hay comentarios
 

Comentar...

Nombre
Correo (no se visualiza en la web)
Valoración
Comentarios
Es necesario revisar y aceptar las políticas de privacidad