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 06 de Agosto del 2017
790 visualizaciones desde el 06 de Agosto del 2017. Una media de 35 por semana
225,0 KB
31 paginas
Creado hace 347d (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