Programación Lógica
Reglas de precedencia entre operadores
?
?, ?
? , ?
?, ?
menor precedencia
Forma Normal de una fórmula
Una fórmula se dice que está en forma normal si todos los cuantificadores han sido desplazados al principio de la fórmula.
Programación Lógica
Forma normal de una fórmula
Una fórmula se dice que está en forma normal si todos los cuantificadores han sido desplazados al principio de la fórmula.
Algunas equivalencias útiles para alcanzar una forma normal
? [ (? X) p(X) ] ? (?X) [? p(X) ]
? [ (?X) p(X) ] ? (? X) [? p(X) ]
(? X) [ p(X) ? q(X) ] ? [ (?X) p(X) ] ? [ (?X) q(X) ]
(? X) [ p(X) ? q(X) ] ? [ (? X) p(X) ] ? [ (? X) q(X) ]
Programación Lógica
Reglas de Inferencia
Especialización Universal: siempre es posible deducir la verificación de un caso concreto a partir de un cuantificador universal.
(?X) p(X) ?p(a)
Sustitución: permite la sustitución de cualquier proposición en una fórmula por otra biequivalente.
Modus ponens: de una implicación de la verificación de la premisa se verifica la conclusión.
Axioma: p ? q
Axioma: p
Teorema: q
Programación Lógica
Modus tollens: de una implicación y de la no verificación del consecuente, se concluye la no verificación de la premisa.
Axioma: p ? q
Axioma: ¬q
Teorema: ¬p
? Introducción: la fbf p?q puede ser inferida de las fbf p y q.
? Eliminación: la fbf p puede ser inferida de la fbf p?q.
? Introducción: la fbf p ? q puede ser inferida de la fbf p o de la fbf q.
Programación Lógica
Lógica de orden cero:
Los predicados carecen de términos y el cálculo de predicados se reduce al cálculo de proposiciones o proposicional.
Lógica de orden uno:
Los predicados poseen términos que pueden ser constantes, variables o functores.
Lógica de orden superior:
Los predicados lógicos pueden ser en sí mismos variables.
Programación Lógica
Ejercicios. Expresar como fbf en lógica de predicados los siguientes hechos
A. Marco era un hombre.
B. Marco era pompeyano (de Pompeya).
C. Todos los pompeyanos eran romanos.
D. César era un dirigente.
E. Todos los romanos o bien eran leales a César o bien le odiaban.
F. Todo el mundo es fiel a alguien.
G. La gente sólo trata de asesinar a aquellos dirigentes a los que no son leales.
H. Marco intentó asesinar a César.
I. Algún romano odia a César.
Programación Lógica
A. hombre(marco)
B. pompeyano(marco)
C. (?X)(pompeyano(X) ? romano(X))
D. dirigente(césar)
E. (?X)(romano(X) ? leal(X,césar) ? odia(X,césar))
F. (?X)(hombre(X) ? ?(?Y) leal(X,Y)?
G. (?X)?(?Y) (hombre(X) ? dirigente(Y)
? intenta_asesinar(X,Y) ? ? leal(X,Y))?
H. intenta_asesinar(marco, césar)
I. (?X) (romano(X) ? odia(X, césar))
Programación Lógica
Teorema + Axiomas (como fórmulas bien formadas, fbf)
Teorema + Axiomas (como cláusulas)
Método de resolución por refutación
Unificación
Demostración automática de teoremas
+
+
Lo que queremos hacer …
Programación Lógica
IMPORTANTE:
La demostración automática de teoremas lógicos es un procedimiento que involucra una mera actividad sintáctica, o de relación entre símbolos, ignorándose completamente el contenido semántico que resulta de la interpretación de las fórmulas.
Programación Lógica
Fórmulas bien formadas (fbf)
Son aquellas que cumplen ciertos requisitos en su estructura y definen la sintaxis del cálculo de predicados
Una fórmula se dice bien formada si puede derivarse de alguna de las siguientes reglas de formación:
1. Cualquier fórmula atómica es una fbf.
2. Si p y q son fbf, entonces también serán fbf las siguientes:
¬p, p ? q, p ? q, p ? q
3. Si X es una variable libre en la fbf p, entonces son fbf :
(?X) p(X), (?X) p(X)
4. Cualquier fórmula que no pueda formarse a partir de estas reglas no es una fbf.
Programación Lógica
Cláusula
Es una fórmula que sólo contiene operadores disyuntivos y posiblemente negaciones sobre los átomos.
Este tipo de fórmulas pueden ser expresadas por una única implicación. Así la fórmula:
a1 ? a2 ? … ? an ? b1 ? b2 ? … ? bm
se puede transformar en :
¬(¬ a1 ? ¬ a2 ? … ? ¬ an ) ? b1 ? b2 ? … ? bm
¬ a1 ? ¬ a2 ? … ? ¬ an ? b1 ? b2 ? … ? bm
Programación Lógica
Cláusulas de Horn.
Aquellas cuyo consecuente tiene un único predicado.
a1 ? a2 ? … ? an ? b
Ventajas de una representación basada en cláusulas de Horn
La demostración de teoremas o resolución de un conjunto de cláusulas de Horn es más sencilla en general.
Las cláusulas de Horn admiten una interpretación directa en términos de un lenguaje de programación, lo que no es posible con cláusulas generales.
Programación Lógica
Transformación a cláusulas
Para ilustrar el proceso paso a paso emplearemos la siguiente fómula compleja como ejemplo:
(?X){p(X) ?{(?Y)[p(Y) ? p(f(X,Y))]? ?(?Y)[q(X,Y) ? p(Y)]}}
1. Eliminar los símbolos de implicación, sustituyendo p ? q por ?p ? q.
Tras este primer paso, nuestra fómula se transforma en:
(?X){?p(X) ? {(?Y)[? p(Y) ? p(f(X,Y))] ? ?(?Y)[? q(X,Y) ? p(Y)]}}
Programación Lógica
2. Mover las negaciones hasta las fórmulas atómicas, para ello se emplean las leyes de Morgan y las transformaciones de cuantificadores existenciales y universales.
? (p ? q) ? ? p ? ? q
? (p ? q) ? ? p ? ? q
? [ (? X) p(X) ] ? (?X) [? p(X) ]
? [ (?X) p(X) ] ? (? X) [? p(X) ]
Aplicándolo sobre el ejemplo:
(?X){?p(X) ? {(?Y)[? p(Y) ? p(f(X,Y))] ? ?(?Y)[? q(X,Y) ? p(Y)]}}
(?X){? p(X) ? {(?Y)[? p(Y) ? p(f(X,Y))] ? (?Y)[q(X,Y) ? ? p(Y)]}}
Programación Lógica
3. Renombrar variables, en aquellos casos en los que varias variables se hayan nombrado de igual forma. En nuestro caso esto ocurre con la variable Y que renombramos como Z en su segunda ocurrencia.
Así nuestro ejemplo se transforma en:
(?X){? p(X) ? {(?Y)[? p(Y) ? p(f(X,Y))] ? (?Y)[q(X,Y) ? ? p(Y)]}}
(?X){? p(X) ? {(?Y)[? p(Y) ? p(f(X,Y))] ? (?Z)[q(X,Z) ? ? p(Z)]}}
Programación Lógica
4. Eliminar los cuantificadores existenciales. Las variables cuantificadas por este tipo de cuantificadores serán sustituidas por un tipo de función comodín denominada función de Skolem (proceso de skolemización).
P.e. (?Z) q(X,Z) se transforma en q(X, g(X))
en donde g(X) es la función de Skolem para este caso. Nótese que no sólo se eliminan los cuantificadores existenciales sino también las variables ligadas a los mismos.
La función de Skolem introducida debe ser nueva en el universo de discurso, y además deberá ser función de todas las variables cuantificadas universalmente cuyos ámbitos incluyan el ámbito del cuantificador existencial que se pretende eliminar.
Programación Lógica
Así nuestro ejemplo se transforma en:
(?X){? p(X) ? {(?Y)[? p(Y) ? p(f(X,Y))] ? (?Z)[q(X,Z) ? ? p(Z)]}}
(?X){? p(X) ? {(?Y)[? p(Y) ? p(f(X,Y))] ? [q(X, g(X)) ? ? p(g(X))]}}
Si el cuantificador existencial no se encuentra en el ámbito de ningún cuantificador universal, se usará una función de Skolem sin argumentos. Como en el siguiente ejemplo:
(?Z) q(Z) se transforma en q(a)
Donde el símbolo constante a referencia a la entidad que sabemos existe. Evidentemente a debe ser un símbolo que no haya sido empeado con anterioridad.
Programación Lógica
5. Desplazar los cuantificadores universales, de manera que queden al comienzo de la fórmula (prenex form). Estre proceso puede ser realizado por cuanto no existen ya variables distintas con el mismo nombre.
(?X){? p(X) ? {(?Y)[? p(Y) ? p(f(X,Y))] ? [q(X, g(X)) ? ? p(g(X))]}}
(?X) (?Y){? p(X) ? { [? p(Y) ? p(f(X,Y))] ? [q(X, g(X)) ? ? p(g(X))]}}
6. Convertir los operadores conjuntivos (AND) en los más externos, para lo que se emplean las leyes distributivas. A la forma resultante se le denomina forma normal conjuntiva.
Este paso se ejecuta sobre el ejemplo en dos pasos:
Programación Lógica
Partiendo de la última expresión,
(?X)(?Y){? p(X) ? { [? p(Y) ? p(f(X,Y))] ? [q(X, g(X)) ? ? p(g(X))]}}
se aplica primero la ley distributiva:
(?X)(?Y){ {? p(X) ? [? p(Y) ? p(f(X,Y))]} ?
{? p(X) ? [q(X, g(X)) ? ? p(g(X))]}}
Aplicando de nuevo la ley distributiva y la asociativa:
(?X)(?Y){ [? p(X) ? ? p(Y) ? p(f(X,Y))] ?
[? p(X) ? q(X, g(X)) ] ?
[? p(X) ? ? p(g(X))]}
Programación Lógica
7. Eliminar los cuantificadores universales. Se trata de una eliminación convencional, no teórica, pues se asume que toda variable que aparezca está cuantificada universalmente. La función de Skolem adquiere sentido, dado que al no aparecer otras variables que las universales, pueden eliminarse sus cuantificadores por convenio. En nuestro ejemplo:
(?X)(?Y){ [? p(X) ? ? p(Y) ? p(f(X,Y))] ?
[? p(X) ? q(X, g(X)) ] ?
[? p(X) ? ? p(g(X))]}
[? p(X) ? ? p(Y) ? p(f(X,Y))] ?
[? p(X) ? q(X, g(X)) ] ?
[? p(X) ? ? p(g(X))]
Programación Lógica
8. Eliminar los conectores conjuntivos (AND).
Dado que la fómula se corresponde con una conjunción de subfómulas, éstas deberán verificarse por separado para que se verifique la fórmula principal.
Esto produce, en nuestro caso, el siguiente conjunto de fórmulas:
[? p(X) ? ? p(Y) ? p(f(X,Y))] ?
[? p(X) ? q(X, g(X)) ] ?
[? p(X) ? ? p(g(X))]
? p(X) ? ? p(Y) ? p(f(X,Y))
? p(X) ? q(X, g(X))
? p(X) ? ? p(g(X))
Programación Lógica
9. Renombrar las variables. para que no aparezca la misma variable en dos cláusulas.
? p(X) ? ? p(Y) ? p(f(X,Y))
? p(X) ? q(X, g(X))
? p(X) ? ? p(g(X))
? p(X) ? ? p(Y) ? p(f(X,Y))
? p(U) ? q(U, g(U))
? p(W) ? ? p(g(W))
—— * * * ——
Mediante este proceso se termina en una representación en forma de cláusulas. Así de una una única fórmula pueden resultar varias cláusulas que son más modulares y de estructura más simple.
Programación Lógica
Proceso de paso a cláusulas
1. Eliminar los símbolos de implicación
2. Mover las negaciones hasta las fórmulas atómicas
3. Renombrar variables
4. Eliminar los cuantificadores existenciales.
5. Desplazar los cuantificadores universales
6. Convertir los operadores AND en los más externos
7. Eliminar los cuantificadores universales.
8. Eliminar los conectores conjuntivos (AND).
9. Renombrar las variables.
Programación Lógica
Un ejemplo del mundo de los bloques
Acerca de los bloques conocemos tres cosas:
A. Que un bloque está encima de algo que no es una pirámide.
B. Que no existe ningún objeto que esté debajo de un bloque y, a la vez, encima del mismo.
C. Que no hay nada que no sea un bloque y que también sea lo mismo que el bloque.
(?X) { bloque(X) ? [(?Y) (encima(X,Y) ? ? piramide(Y))
? ? (?Y) (encima(X,Y) ? encima(Y,X))
? (?Y) (? bloque(Y) ? ? igual(X,Y))]}
Programación Lógica
0. La fórmula inicial
(?X) { bloque(X) ? [ (?Y) (encima(X,Y) ? ? piramide(Y))
? ? (?Y) (encima(X,Y) ? encima(Y,X))
? (?Y) (? bloque(Y) ? ? igual(X,Y))]}
1. Eliminar las implicaciones
(?X) {? bloque(X) ? [ (?Y) (encima(X,Y) ? ? piramide(Y))
? ? (?Y) (encima(X,Y) ? encima(Y,X))
? (?Y) (bloque(Y) ? ? igual(X,Y))]}
2. Mover las negaciones hasta las fórmulas atómicas
(?X) {? bloque(X) ? [ (?Y) (encima(X,Y) ? ? piramide(Y))
? (?Y) (? encima(X,Y) ? ? encima(Y,X))
? (?Y) (bloque(Y) ? ? igual(X,Y))]}
Programación Lógica
3. Renombrar las variables
(?X) {? bloque(X) ? [ (?Y) (encima(X,Y) ? ? piramide(Y))
? (?Z) (? encima(X,Z) ? ? encima(Z,X))
? (?W) (bloque(W) ? ? igual(X,W))]}
4. Eliminar los cuantificadores existenciales
(?X) {? bloque(X) ? [ (encima(X,g(X)) ? ? piramide(g(X)))
? (?Z) (? encima(X,Z) ? ? encima(Z,X))
? (?W) (bloque(W) ? ? igual(X,W))]}
5. Desplazar los cuantificadores universales
(?X)(?Z)(?W){? bloque(X) ? [ (encima(X,g(X)) ? ? piramide(g(X)))
? (? encima(X,Z) ? ? encima(Z,X))
? (bloque(W) ? ? igual(X,W))]}
Programación Lógica
6. Convertir los operadores AND en los más externos
(?X)(?Z)(?W){? bloque(X) ? [ (encima(X,g(X)) ? ? piramide(g(X)))
? (? encima(X,Z) ? ? encima(Z,X))
? (bloque(W) ? ? igual(X,W))]}
paso 1.
(?X)(?Z)(?W){(? bloque(X) ? (encima(X,g(X)) ? ? piramide(g(X))))
? (? bloque(X) ? ? encima(X,Z) ? ? encima(Z,X))
? (? bloque(X) ? bloque(W) ? ? igual(X,W))]}
paso 2.
(?X)(?Z)(?W){(? bloque(X) ? encima(X,g(X)))
? (? bloque(X) ? ? piramide(g(X)))
? (? bloque(X) ? ? encima(X,Z) ? ? encima(Z,X))
? (? bloque(X) ? bloque(W) ? ? igual(X,W))]}
Programación Lógica
7. Eliminar los cuantificadores universales
(? bloque(X) ? encima(X,g(X)))
? (? bloque(X) ? ? piramide(g(X)))
? (? bloque(X) ? ? encima(X,Z) ? ? encima(Z,X))
? (? bloque(X) ? bloque(W) ? ? igual(X,W))
8. Eliminar los conectores AND
? bloque(X) ? encima(X,g(X))
? bloque(X) ? ? piramide(g(X))
? bloque(X) ? ? encima(X,Z) ? ? encima(Z,X)
? bloque(X) ? bloque(W) ? ? igual(X,W)
Programación Lógica
9. Renombrar las variables
? bloque(X) ? encima(X,g(X))
? bloque(Y) ? ? piramide(g(Y))
? bloque(U) ? ? encima(U,Z) ? ? encima(Z,U)
? bloque(V) ? bloque(W) ? ? igual(V,W)
Nótese que la función de Skolem tiene la semántica de identificar el apoyo de X. Si la renombramos a “soporte(X)” y representamos las cláusulas como implicaciones obtenemos:
bloque(X) ? encima(X, soporte(X))
bloque(Y) ? ? piramide(soporte(Y))
bloque(U) ? encima(U,Z) ? ? encima(Z,U)
bloque(V) ? ? bloque(W) ? ? igual(V,W)
Programación Lógica
A. hombre(marco)
B. pompeyano(marco)
C. (?X)(pompeyano(X) ? romano(X))
D. dirigente(césar)
E. (?X)(romano(X) ? leal(X,césar) ? odia(X,césar))
F. (?X)(hombre(X) ? ?(?Y) leal(X,Y)?
G. (?X)?(?Y) (hombre(X) ? dirigente(Y)
? intenta_asesinar(X,Y) ? ? leal(X,Y))?
H. intenta_asesinar(marco, césar)
I. (?X) (romano(X) ? odia(X, césar))
Programación Lógica
Proceso de paso a cláusulas
1. Eliminar los símbolos de implicación
A. hombre(marco)
B. pompeyano(marco)
C. (?X)(? pompeyano(X) ? romano(X))
D. dirigente(césar)
E. (?X)(? romano(X) ? leal(X,césar) ? odia(X,césar))
F. (?X)(? hombre(X) ? ?(?Y) leal(X,Y)?
G. (?X){ (?Y) ? ? (hombre(X) ? dirigente(Y) ? intenta_asesinar(X,Y) ?
? ? leal(X,Y)) }
H. intenta_asesinar(marco, césar)
I. (?X) (romano(X) ? odia(X, césar))
Programación Lógica
Proceso de paso a cláusulas
2. Mover las negaciones hasta las fórmulas atómicas
A. hombre(marco)
B. pompeyano(marco)
C. (?X)(? pompeyano(X) ? romano(X))
D. dirigente(césar)
E. (?X)(? romano(X) ? leal(X,césar) ? odia(X,césar))
F. (?X)(? hombre(X) ? ?(?Y) leal(X,Y)?
G. (?X)(?Y)
(? hombre(X)? ? dirigente(Y) ? ? intenta_asesinar(X,Y) ? ? leal(X,Y))
H. intenta_asesinar(marco, césar)
I. (?X) (romano(X) ? odia(X, césar))
3. Renombrar las variables
Programación Lógica
Proceso de paso a cláusulas
4. Eliminar los cuantificadores existenciales
A. hombre(marco)
B. pompeyano(marco)
C. (?X)(? pompeyano(X) ? romano(X))
D. dirigente(césar)
E. (?X)(? romano(X) ? leal(X,césar) ? odia(X,césar))
F. (?X)(? hombre(X) ? leal(X, g(X))
G. (?X)(?Y)
(? hombre(X)? ? dirigente(Y)? ? intenta_asesinar(X,Y)? ? leal(X,Y))
H. intenta_asesinar(marco, césar)
I. romano(f) ? odia(f, césar))
Programación Lógica
Proceso de paso a cláusulas
5. Desplazar los cuantificadores universales
6. Convertir los operadores AND en los más externos
A. hombre(marco)
B. pompeyano(marco)
C. (?X)(? pompeyano(X) ? romano(X))
D. dirigente(césar)
E. (?X)(? romano(X) ? leal(X,césar) ? odia(X,césar))
F. (?X)(? hombre(X) ? leal(X, g(X))
G. (?X)(?Y)
(? hombre(X)? ? dirigente(Y)? ? intenta_asesinar(X,Y)? ? leal(X,Y))
H. intenta_asesinar(marco, césar)
I. romano(f) ? odia(f, césar))
Programación Lógica
Proceso de paso a cláusulas
7. Eliminar los cuantificadores universales
A. hombre(marco)
B. pompeyano(marco)
C. ? pompeyano(X) ? romano(X)
D. dirigente(césar)
E. ? romano(X) ? leal(X,césar) ? odia(X,césar)
F. ? hombre(X) ? leal(X, g(X))
G. ? hombre(X) ? ? dirigente(Y) ? ? intenta_asesinar(X,Y) ? ? leal(X,Y)
H. intenta_asesinar(marco, césar)
I. romano(f) ? odia(f, césar))
Programación Lógica
Proceso de paso a cláusulas
8. Eliminar los conectores AND
A. hombre(marco)
B. pompeyano(marco)
C. ? pompeyano(X) ? romano(X)
D. dirigente(césar)
E. ? romano(X) ? leal(X,césar) ? odia(X,césar)
F. ? hombre(X) ? leal(X, g(X))
G. ? hombre(X) ? ? dirigente(Y) ? ? intenta_asesinar(X,Y) ? ? leal(X,Y)
H. intenta_asesinar(marco, césar)
I1. romano(f)
I2. odia(f, césar))
Programación Lógica
Proceso de paso a cláusulas
8. Renombrar las variables
A. hombre(marco)
B. pompeyano(marco)
C. ? pompeyano(X) ? romano(X)
D. dirigente(césar)
E. ? romano(Y) ? leal(Y,césar) ? odia(Y,césar)
F. ? hombre(Z) ? leal(Z, g(Z)
G. ? hombre(W) ? ? dirigente(K) ? ? intenta_asesinar(W,K) ? ? leal(W,K)
H. intenta_asesinar(marco, césar)
I1. romano(f)
I2. odia(f, césar))
Programación Lógica
Teorema + Axiomas (como fórmulas bien formadas, fbf)
Teorema + Axiomas (como cláusulas)
Método de resolución por refutación
Unificación
Demostración automática de teoremas
+
+
Lo que queremos hacer …
Unificación
Programación Lógica
Unificación y sustitución
Ejemplos:
Definir las sustituciones necesarias para unificar el predicado
p(X, f(Y), b)
con cada uno de los siguientes predicados:
P1: p(g(Z), f(a), b)
P2: p(X, f(a), b)
P3: p(Z, f(U), b)
P4: p(c, f(a), b)
Programación Lógica
Unificación y sustitución
El proceso de unificación determina las condiciones y posibilidades de sustitución de un predicado por otro. Por ejemplo, en el caso de los siguientes axiomas:
p(X) ? q(X)
p(a)
la demostración de q(a) es consecuencia de la regla de especialización Universal aplicada a:
p(X) ? q(X)
para producir
p(a) ? q(a)
También puede interpretarse como que se ha procedido a realizar la sustitución de p(X) por p(a), previa unificación de X con a.
El proceso de sustitución de términos, denominado Unificación, para lograr que dos expresiones sean idénticas es fundamental en el proceso de demostración de teoremas en la lógica de predicados de primer orden.
Programación Lógica
Unificación y sustitución
Un proceso de unificación puede ser representado mediante un operador ? constituido por un conjunto de de pares de términos ordenados por:
? = { v1? t1, v2? t2, …, vn? tn}
donde el par vi? ti, indica que la variable vi es sustituida por el término ti.
Así el predicado p se transforma mediante la sustitución indicada por ? en p(… , vk, …) ? = p(… , tk, …).
NOTA: También es muy habitual la notación equivalente
? = { v1/ t1, v2/ t2, …, vn/ tn}
Programación Lógica
Unificación y sustitución
Ejemplos:
Definir las sustituciones necesarias para unificar el predicado
p(X, f(Y), b)
con cada uno de los siguientes predicados:
P1: p(g(Z), f(a), b)
P2: p(X, f(a), b)
P3: p(Z, f(U), b)
P4: p(c, f(a), b)
?1 = { X ? g(Z), Y ? a }
?2 = { Y ? a }
?3 = { X ? Z, Y ? U }
?4 = { X ? c, Y ? a }
Programación Lógica
Unificación y sustitución
El proceso de unificación implica la sustitución de una variable por otro término que puede ser variable, constante o functor. En este último caso, el functor no puede contener la variable sustituida.
Es evidente que no siempre es posible unificar dos realizaciones de un mismo predicado. Por ejemplo q(a, f(X), X) y q(c, f(d), b)
no son unificables.
La composición de dos sustituciones ?1 y ?2, se denota por ?1 ?2 y es la sustitución que resulta de aplicar la sustitución ?2 a los términos de ?1 y de añadir a continuación los pares de sustituciones de ?2 sobre las variables no contenidas entre las variables de ?1.
{ Z ? f(X,Y), U ? X } { X ? a, Y ? b, W ? c, Z ? d } ?
{ Z ? f(a,b), U ? a, X ? a, Y ? b, W ? c }
Programación Lógica
Unificación y sustitución
Se puede demostrar que :
A. [L?1]?2 = L [?1?2]
B. (?1?2) ?3 = ?1 (?2?3), Asociatividad
C. ?1?2 ? ?2?1 no es conmutativa
Diremos que dos predicados, E1 y E2, son unificables, y lo representaremos por {E1, E2}, si existe una sustitución ? tal que se verifica:
E1 ? = E2 ?
A la sustitución ? la denominaremos Unificador de E1 y E2.
Ejemplo: Dados p(X, f(Y), b) y p(X, f(b), b) y la sustitución
? = { X ? a, Y ? b }, decimos que ? es un unificador de estos dos predicados porque los convierte en p(a, f(b), b).
Programación Lógica
Unificación y sustitución
Aunque ? = { X ? a, Y ? b } es un unificador de estos dos predicados no es el más simple de los unificadores posibles (se le podría denominar alternativamente “más general”) para este conjunto, que este caso sería ? = { Y ? b }.
Así si ? es el unificador más simple de { Ei } se verifica que si ? es un unificador de { Ei } entonces existe una sustitución s tal que:
{ Ei } ? s = { Ei } ?
Un algoritmo recursivo nos permite descubrir si dos predicados son unificables o no, y, en su caso, hallar el unificador más simple.
Programación Lógica
Algoritmo de Unificación
Etapas del algoritmo.
1. Comprobaremos si los símbolos de los predicados son los mismos. En caso negativo los predicados no son unificables.
2. Si los predicados son iguales, han de tener la misma aridad (nº de argumentos). En caso negativo los predicados no son unificables.
3. Comprobaremos los argumentos por pares correspondientes, aplicando el algoritmo recursivamente (es necesario si los argumentos contienen functores), abortando el proceso desde el momento en que un par de argumentos no sea unificable.
Programación Lógica
Algoritmo de Unificación
Unifica(e1, e2) {
1. Si e1 o e2 son ambos variables o constantes, entonces
1.a Si e1 y e2 son idénticos, entonces devolver { }.
1.b Si e1 es una variable, entonces
1.b.1 Si e1 aparece dentro de e2 entonces devolver {FALLO}
en otro caso, devolver { e1 ? e2 }.
1.c Si e2 es una variable, entonces
1.c.1 Si e2 aparece dentro de e1 entonces devolver {FALLO}
en otro caso, devolver { e2 ? e1 }.
1.d Devolver {FALLO}
2. Si los símbolos de los predicados e1 y e2 son diferentes o tienen diferente aridad entonces devolver {FALLO}.
3. Hacer SUBS = NIL (al final del proceso SUBS contendrá las sustituciones necesarias para unificar e1 y e2).
(continúa …)
Programación Lógica
Algoritmo de Unificación
Unifica(e1, e2) {
…
4. Para cada uno de los argumentos de e1 (indexados por i)
4.a Invocar Unifica con los i-ésimos argumentos de e1 y e2, poniendo el
resultado en s.
4.b Si s es igual a FALLO, entonces devolver {FALLO}.
4.c Si s es diferente de { }, entonces
4.c.1 Aplicar la sustitución s sobre el resto de argumentos de e1 y e2
4.c.2 Añadir s a las sustituciones ya contenidas en SUBS.
5. Devolver SUBS.
}
Programación Lógica
Algoritmo de Unificación
Ejercicios: Tracear la operación del algoritmo de unificación para cada uno de los siguientes pares de predicados.
A. f(marcos), f(césar)
B. f(X), f(g(Y))
C. f(marcos, g(X,Y)), f(X, g(césar, marcos))
D. p(X, X), p( g(X), g(X))
E. p(X, X), p( Y, g(X))
F. p(X, f(x)), p(Y, Y)
G. p(Y, Y, b), p(Z, X, Z)
H. p(f(X,X), a), p(f(Y, f(Y,a)), a)
Programación Lógica
Resolución por refutación
Método de demostración de teoremas
Robinson, 1965
Basado en el principio de refutación
Relativamente sencillo de automatizar
IDEA.
Si queremos demostrar un teorema dado en base a un conjunto de axiomas que suponemos consistente, podemos hacerlo mostrando que el conjunto formado por la negación del teorema y el conjunto de axiomas es inconsistente.
Si tal inconsistencia se demuestra será porque el teorema era cierto.
Programación Lógica
Decidibilidad y Consistencia
Sistema formal:
Validez de
una expresión:
Decidibilidad:
Un conjunto de expresiones básicas y un conjunto de reglas de generación de nuevas expresiones
Se dice que una expresión es válida en un sistema formal si es posible derivar la misma a partir de las expresiones básicas
Un sistema formal U se dice decible si existen procedimientos efectivos para determinar la validez dentro de U de las expresiones V y ?V
procedimientos efectivos : desarrollos que involucran un número finito de operaciones elementales y de posiciones de memoria
Programación Lógica
Decidibilidad y Consistencia
Indecidibilidad:
Semi-decibilidad:
Consistencia:
Un sistema formal U se dice indecible si no es posible determinar la validez V y ?V de forma efectiva
Cuando sólo es posible determinar de forma efectiva la validez de una de las expresiones V o ?V
Un sistema formal U se dice consistente en sentido fuerte, si sólo una de las expresiones V o ?V es válida en U. Es evidente que un sistema consistente debe ser Decible.
Programación Lógica
Decidibilidad y Consistencia
Inconsistencia:
Un sistema formal U se dice inconsistente si ambas expresiones V y ?V son válidas en U.
Un sistema lógico L compuesto de fórmulas básicas o axiomas y reglas de inferencia constituye un sistema formal.
Un sistema lógico L que contiene las expresiones F y ?F constituye un sistema inconsistente por cuanto F y ?F son válidas en L.
Programación Lógica
Decidibilidad y Consistencia
Se han desarrollado procedimientos efectivos capaces de demostrar la inconsistencia de un sistema lógico. Sin embargo, no existen tales procedimientos para demostrar su consistencia.
Por ello un sistema lógico es un sistema Semi-decible y no pueden definirse criterios de consistencia fuerte, usándose en su defecto otro criterio de consistencia débil.
Definición: un sistema lógico que no es Inconsistente se dice que es consistente en sentido débil
Programación Lógica
Decidibilidad y Consistencia
Si A es un conjunto de cláusulas lógicas consistentes, denominadas Axiomas, y T es otra cláusula, denominada Teorema, entonces si T es una consecuencia lógica de A se debe verificar:
1. El conjunto A ? T es consistente
2. El conjunto A ? ?T es inconsistente
Sólo la segunda propiedad es verificable de forma efectiva, de donde se deduce intuitivamente un procedimiento de demostración de teoremas que consiste en demostrar la inconsistencia de A ? ?T . A este procedimiento se le denomina de Resolución por Refutación del Teorema.
Programación Lógica
Cláusula resolvente
Sean dos cláusulas, que denominaremos cláusulas padres, que contengan respectivamente, una misma proposición, negada y sin negar, cada una de ellas. Como es el caso de la proposición p1 en el siguiente ejemplo:
p1 v p2 v … v pn
? p1 v q2 v … v qm
Ambas cláusulas forman parte de un sistema que se asume consistente y, por tanto, son ciertas. Puede construirse entonces una nueva cláusula, denominada cláusula resolvente a partir de la disyunción de ambas eliminando la proposición que aparece doblemente. Esto es:
(p1 v p2 v … v pn) v (? p1 v q2 v … v qm)
? (p1 v ? p1) v (p2 v … v pn v q2 v … v qm)
? p2 v … v pn v q2 v … v qm
Programación Lógica
Cláusula resolvente
La nueva cláusula (cláusula resolvente) debe ser cierta por cuanto las cláusulas padre forman un conjunto de cláusulas consistente con lo que el conjunto que resulta de añadir la cláusula resolvente al conjunto de cláusulas anterior sigue siendo consistente.
Los siguientes son algunos ejemplos de la aplicación del método de la cláusula resolvente:
(? p v q) v p ? q (modus ponens)
(p v q) v (? p v q) ? q
(? p v p) ? nil (inconsistencia)
(? p v q) v (? q v r) ? ? p v r (encadenamiento de reglas)
(p v ? q) v (? p v q) ? q v ? q (tautología)
Nótese que en el último caso, también podría resolverse sobre q y obtendríamos como cláusula resolvente p v ? p. Lo que no es correcto es resolver doblemente sobre p y q y obtener un resolvente nulo.
Programación Lógica
Cláusula resolvente
(p v ? q) v (? p v q) ? q v ? q (tautología)
Una forma de ver que la doble resolución es un error es considerar el caso sencillo anterior cuando se resuelve doblemente. En ese caso obtendríamos la cláusula nula, indicando una inconsistencia. Sin embargo, podemos comprobar que ambas cláusulas son consistentes cuando ambos predicados son verdaderos, lo que indica que la conclusión de inconsistencia que se deriva de la doble resolución es incorrecta.
La idea que subyace en el método de resolución se basa en que la fórmula ((p v ?) ? (? p v ?)) ? (? v ?) es una tautología (demostrarlo empleando una tabla de verdad).
Por el contrario, puede comprobarse que la fórmula similar que debería sustentar la doble resolución, ((p v r v ?) ? (? p v ? r v ?)) ? (? v ?) , donde r es q o ? q, no es válida.
Programación Lógica
Resolución por Refutación
La resolución por refutación consiste esencialmente en aplicar el método de la cláusula resolvente para eventualmente alcanzar el resolvente nulo. Si esto es posible se habrá demostrado la inconsistencia del conjunto formado por los axiomas (cuya validez está garantizada) y el teorema negado, en cuyo caso el teorema se considera demostrado.
? a v b
? b v c
a
? c
? a v c
c
nil
Programación Lógica
Resolución por Refutación
Para poder aplicar el método de la cláusula resolvente a predicados y no sólo a proposiciones es preciso primeramente unificar las cláusulas para conseguir que los términos de los predicados complementarios sean idénticos.
Ejemplo: Sean las siguientes cláusulas padre.
p(X, f(a)) ? p(X, f(Y)) ? q(Y)
? p(Z, f(a)) ? ? q(Z)
Se puede encontrar un resolvente empleando bien p o bien q como predicados complementarios. Si elegimos p, el unificador será:
{ p(X, f(a)), p(Z, f(a)) } con la sustitución ? = { X ? Z }
que produce la cláusula resolvente:
p(Z, f(Y)) ? q(Y) ? ? q(Z)
Programación Lógica
Resolución por Refutación
Otra forma de generar una cláusula resolvente más sencilla consiste en eliminar alguna de las realizaciones del mismo predicado p en alguna de las cláusulas padre. Por ejemplo, encontrando un unificador y absorbiendo una de las realizaciones.
p(X, f(a)) ? p(X, f(Y)) ? q(Y)
? p(Z, f(a)) ? ? q(Z)
Así : { p(X, f(a)), p(X, f(Y)) } con la sustitución ? = { Y ? a }
convierte las cláusulas padre en:
p(X, f(a)) ? q(a)
? p(Z, f(a)) ? ? q(Z)
Aplicando el unificador ? = { Z ? X } resolviendo, obtenemos como resolvente:
q(a) ? ? q(X)
Programación Lógica
Resolución por Refutación
Una idea clave:
Si el par de cláusulas padre se toma de un conjunto de cláusulas consistentes, entonces, dado que la cláusula resolvente es una consecuencia lógica de las anteriores, también es consistente el conjunto resultante de añadir el resolvente al conjunto original.
Programación Lógica
Resolución por Refutación
Idea sobre la que se desarrolla el algoritmo:
Hasta que se encuentre la cláusula nula se exploran pares de cláusulas padre, incluyendo – en caso de fracaso – el resolvente en el conjunto de cláusulas.
El proceso para si:
1. El resolvente generado es nulo: se ha demostrado el teorema.
2. Si no existe ningún par de cláusulas que puedan producir un resolvente, entonces no se puede demostrar la inconsistencia del conjunto y se dice que el conjunto no es completo. Esto significa que el teorema no es una consecuencia lógica de los axiomas y, por tanto, se puede suponer falso.
Programación Lógica
Algoritmo: Resolución por Refutación
0. Se supone que tanto los axiomas como la negación del teorema han sido transformados en cláusulas.
1. Incluir en el conjunto de cláusulas TRABAJO el conjunto de axiomas y el teorema negado.
2. Repetir hasta que se produzca la cláusula nula, o no se encuentre ningún resolvente:
2.a Encontrar en TRABAJO un par de cláusulas que puedan resolverse y obtener el resolvente. Eliminar los elementos duplicados.
2.b Descartar la cláusula si contiene un predicado y su negación.
2.c Si el resolvente no está en TRABAJO, añadirlo.
3. Si se ha encontrado la cláusula nula, el teorema es cierto. En caso contrario, el teorema se supone falso.
Programación Lógica
Ejemplo:
Axiomas.
A.1 “Cualquiera que puede leer es un ilustrado”
A.2 “Los delfines no son ilustrados”
A.3 “Algunos delfines son inteligentes”
Teorema.
T. “Algunos que son inteligentes, no pueden leer”
Axiomas
A.1 “Cualquiera que puede leer es un ilustrado”
(?X)(r(X) ? l(X))
A.2 “Los delfines no son ilustrados”
(?X)(d(X) ? ? l(X))
A.3 “Algunos delfines son inteligentes”
(?X)(d(X) ? i(X))
Teorema.
T. “Algunos que son inteligentes, no pueden leer”
(?X)(i(X) ? ? r(X))
Programación Lógica
Ejemplo: Paso a cláusulas
Axiomas
A.1 (?X)(r(X) ? l(X))
A.2 (?X)(d(X) ? ? l(X))
A.3 (?X)(d(X) ? i(X))
Teorema.
T. (?X)(i(X) ? ? r(X))
? r(X) ? l(X)
? d(Y) ? ? l(Y)
d(a)
i(a)
donde a es una función de Skolem constante
? i(Z) ? r(Z)
Programación Lógica
Ejemplo: Grafo de resolución
? r(X) ? l(X)
? d(Y) ? ? l(Y)
d(a)
? i(Z) ? r(Z)
i(a)
r(a)
l(a)
? d(a)
{ }
{Z? a}
{X? a}
{Y? a}
Programación Lógica
El proceso de resolución puede simplificarse si , previamente o durante el proceso se realizan determinadas eliminaciones de cláusulas, lo que equivale a una poda del árbol de exploración.
1. Eliminación de tautologías. Eliminación de cláusulas tales que puedan ser reducidad a una tautología.
p(A) ? q(B) ? ¬ q(B)
2. Eliminación por absorción. Por definición, una cláusula {Li} absorbe a otra {Mi} si existe una sustitución s tal que {Li}s es un subconjunto de {Mi}.
p(X) elimina a p(Y) ? q(U)
p(X) elimina a p(a)
p(X) elimina a p(b) ? q(Z)
p(X) ? q(W) elimina a p(f(a,b)) ? q(g(T)) ? r(V)
3. Eliminación procedimental. Cuando un predicado puede ser evaluado (debido a mecanismos extralógicos o de tipo procedimental) y se evalúa a cierto entonces es posible eliminar la cláusula que lo contiene. Si se evalúa a falso, entonces simplemente se puede eliminar ese predicado de la cláusula.
Programación Lógica
El proceso de resolución descrito previamente es claramente un sistema de exploración de alternativas.
ESTADOS: Cada estado está constituido por la situación del conjunto de cláusulas.
estado inicial: conjunto de axiomas+teorema negado
…
estado final: cláusula nula.
OPERADORES: Generan nuevas cláusulas.
* Considerando diferentes pares de cláusulas padres
* Considerando un mismo para de cláusulas padres, pero unificándolas de diferentes maneras.
Programación Lógica
Para realizar todo el proceso de exploración es necesario disponer de una estrategia que indique en cada situación qué acción realizar, básicamente, como seleccionar los pares de cláusulas padres.
Veremos las siguientes estrategias de control:
Estrategia por niveles
Estrategia del conjunto soporte
Estrategia de la Unidad Preferente
Estrategia de Entrada Lineal
Programación Lógica
Estrategia por Niveles
A partir del conjunto de cláusulas
1. Se calculan todos los posibles resolventes
2. Se añaden éstos a la base de datos
3. ¿Algún resolvente es la cláusula nula?. En caso afirmativo terminar. En otro caso volver a 1.
? r(X) ? l(X)
? d(Y) ? ? l(Y)
d(a)
? i(Z) ? r(Z)
i(a)
r(a)
? i(Z) ? l(Z)
? r(Y) ? ? d(Y)
? l(a)
l(a)
? d(a)
l(a)
? i(Z) ? ? d(Z)
? r(a)
? i(a)
? i(Z) ? ? d(Z)
{}
X
X
Programación Lógica
Estrategia del Conjunto Soporte
El primer nivel de resolventes se genera teniendo como cláusula padre a la cláusula que resulta de negar el teorema.
Posteriormente, para el resto de resolventes siempre se toma como mínimo un padre del conjunto de resolventes ya generado, al que se denomina conjunto soporte. De esta manera todos los resolventes son descendientes de la cláusula del teorema.
El fundamento de esta estrategia radica en que si se alcanza la cláusula nula se deberá a la cláusula del teorema, ya que es ésta la que podrá generar la inconsistencia del conjunto.
Programación Lógica
? r(X) ? l(X)
? d(Y) ? ? l(Y)
d(a)
? i(Z) ? r(Z)
i(a)
r(a)
? i(Z) ? l(Z)
l(a)
? i(Z) ? ? d(Z)
l(a)
? d(a)
? i(a)
? d(a)
? d(a)
{}
X
X
X
Programación Lógica
Estrategia de la Unidad Preferente
Modificación de la estrategia del Conjunto Soporte en la que sólo se genera un resolvente por nivel. Para formarlo se toma una cláusula padre del conjunto de resolventes y otra que se pueda resolver con él. Evidentemente en el primer nivel se tomará la cláusula del teorema como una de las cláusulas padre.
? r(X) ? l(X)
? d(Y) ? ? l(Y)
d(a)
? i(Z) ? r(Z)
i(a)
r(a)
l(a)
? d(a)
{}
Programación Lógica
Estrategia de Entrada Lineal
En esta estrategia se toma como mínimo una cláusula del conjunto de cláusulas iniciales. Esta estrategia no es completa, y puede no ser adecuada en todos los problemas por cuanto puede conducir a una situación en la que no se pueda continuar con la refutación, aunque el teorema sea cierto.
? r(X) ? l(X)
? d(Y) ? ? l(Y)
d(a)
? i(Z) ? r(Z)
i(a)
r(a)
? i(Z) ? l(Z)
? r(Y) ? ? d(Y)
? l(a)
l(a)
l(a)
? i(Z) ? ? d(Z)
? r(a)
? i(Z) ? ? d(Z)
X
X
¬ i(a)
{}
Programación Lógica
Obtención de respuestas
El procedimiento de Resolución por Refutación demuestra teoremas del tipo (?X) p(X) para los que, además de concluir si el teorema es verdadero o falso, interesa conocer el valor de X que satisface el teorema.
A este proceso se le denomina obtención de repuestas
Se pueden emplear dos procedimientos
Programación Lógica
Obtención de respuestas
Procedimiento A:
1. Demostrar el teorema por el procedimiento ya explicado.
2. Añadir al conjunto de cláusulas inicial, no el teorema negado (?p(X)), sino la disyunción de éste con su negado, es decir, (?p(X) ? p(X)) (una tautología).
3. Seguir los mismos pasos que condujeron a la demostración del teorema. Dado que la cláusula del teorema contiene una tautología no se concluirá en el resolvente nulo, sino que se concluirá en la cláusula del teorema.
4. La respuesta es el resolvente final.
Programación Lógica
Ejemplo:
Axiomas: A1. (?X)( juega(pedro, X) ? juega(luis, X))
A2. juega(pedro, fútbol).
Teorema: T. (?X) juega(luis, X)
El problema consiste en demostrar el teorema y, además, en saber a qué juega luis.
Programación Lógica
Expresados en forma clausular y negando el teorema:
A1. ? juega(pedro, X) ? juega(luis, X))
A2. juega(pedro, fútbol).
?T. ? juega(luis, Y)
El árbol de refutación sería:
? juega(luis, Y)
? juega(pedro, X) ? juega(luis, X)
juega(pedro, fútbol).
? juega(pedro, X)
{}
{Y?X}
{X?fútbol}
Programación Lógica
Y la obtención de la respuesta sería:
? juega(luis, Y) ? juega(luis, Y)
? juega(pedro, X) ? juega(luis, X)
juega(pedro, fútbol).
? juega(pedro, X) ? juega(luis, X)
juega(luis, fútbol)
{Y?X}
{X?fútbol}
Programación Lógica
Puede generalizarse el procedimiento anterior de manera que en lugar de incluir la tautología (?p(X) ? p(X)), se incluya la cláusula:
(?p(X) ? respuesta(X))
donde “respuesta” es un predicado comodín, que no puede aparecer en el conjunto de axiomas.
Dado que este predicado no aparece en el resto del conjunto es imposible que pueda desaparecer del árbol modificado de refutación y, por tanto, no se concluirá en la cláusula nula.
Programación Lógica
Obtención de respuestas
Procedimiento B:
1. Añadir al conjunto de cláusulas de los axiomas la cláusula (?p(X) ? respuesta(X)). El predicado comodín debe contener tantos términos como respuestas se deseen, p.e.
(?p(X,Y) ? respuesta(X,Y))
2. Realizar la demostración del teorema, utilizando como objetivo no la cláusula nula, sino una cláusula que contiene solamente el predicado comodín “respuesta”.
3. Las respuestas son los términos del predicado comodín en el estado final.
Programación Lógica
Con este procedimiento, la obtención de la respuesta sería:
? juega(luis, Y) ? respuesta(Y)
? juega(pedro, X) ? juega(luis, X)
juega(pedro, fútbol).
? juega(pedro, X) ? respuesta(X)
respuesta(fútbol)
{Y?X}
{X?fútbol}
Programación Lógica
Problema:
A partir del siguiente conjunto de axiomas,
A1. ?X (c(X) ? s(X))
A2. ?X (? g(X) ? d(X))
A3. ? (?X (g(X) ? ? c(X)))
Aplicar el método de resolución por refutación para demostrar los siguientes teoremas:
TEOREMA 1. ?X (s(X) ? d(X))
TEOREMA 2. ?X (? s(X) ? d(X))
NOTA: Es importante detallar bien cada paso del proceso de demostración
Programación Lógica
Problema:
Convirtiendo en cláusulas:
A1. ? c(X) ? s(X)
A2. g(Y) ? d(Y)
A3. ? g(Z) ? c(Z)
Negando los teoremas:
? T1. ? (?X (s(X) ? d(X)))
? T2. ? (?X (? s(X) ? d(X)))
Conviertiendo los teoremas negados en cláusulas:
? T1. ? s(f) ? ? d(f)
? T2. ? s(f)
? d(f)
Programación Lógica
Resolvamos primero para el T2
? c(X) ? s(X)
g(Y) ? d(Y)
? g(Z) ? c(Z)
? d(f)
g(f)
c(f)
s(f)
? s(f)
{}
{Y? f}
{Z? f}
{X? f}
Programación Lógica
Resolvamos para el T1
? c(X) ? s(X)
g(Y) ? d(Y)
? g(Z) ? c(Z)
? s(f) ? ? d(f)
? s(f) ? g(f)
? s(f) ? c(f)
? c(f) ? c(f)
OJO: No se puede resolver doblemente
{Y? f}
{Z? f}
{X? f}
Programación Lógica
Sistemas de Deducción
Un conjunto de procedimientos de demostración de teoremas que utilizan esquemas diferentes al de refutación.
Procedimientos directos: porque emplean el conjunto de axiomas y el teorema sin negar
Como estrategia de control: exploración de alternativas.
Sistemas de deducción “Hacia-Delante”
Sistemas de deducción “Hacia-Atrás”
Programación Lógica
Sistemas de Deducción
S.D. Hacia-Delante:
Se parte de los axiomas y se trata de llegar al teorema por aplicación de reglas de inferencia.
Evidentemente, ésto sólo será posible si el teorema es una consecuencia lógica de los axiomas.
S.D. Hacia-Atrás:
Se parte del teorema y, por aplicación de reglas de inferencia, se intenta llegar a unos hechos completamente ciertos.
Programación Lógica
Hechos, Reglas y Objetivos
Los elementos que intervienen en la deducción son:
Reglas: Son aquellos axiomas que contienen una implicación, con antecedentes y consecuentes
Hechos: Se denominan así a los axiomas que no contienen una implicación. Son elementos sin condiciones.
Meta u Objetivo: Designa al teorema a demostrar.
Programación Lógica
Hechos, Reglas y Objetivos
Nomenclatura de Kowalsky:
Reglas: b1 ? b2 ? b3 ? … ? bm ? a1 ? a2 ? … ? an
Hechos: b1 ? b2 ? b3 ? … ? bm ?
Meta u Objetivo: ? a1 ? a2 ? … ? an
donde ai y ? bj representan predicados lógicos
Programación Lógica
Hechos, Reglas y Objetivos
Se puede simplificar esta nomenclatura si se admite la sustitución de operadores por comas que el antecedente representarán conjunciones y el consecuente disyunciones. Si nos restrigimos, además, a considerar sólo cláusulas de Horn:
Reglas: b ? a1 , a2 , … , an
Hechos: b ?
Meta u Objetivo: ? a1 , a2 , … , an
Programación Lógica
Deducción progresiva o Hacia-Delante
Se parte de los hechos como elementos básicos de transformación. Intuitivamente, el procedimiento puede resumirse de la siguiente forma, suponiendo que a1 es un predicado unificable con algún antecedente o subobjetivo:
a1 ?
c ? a1 , a2 , … , an
? a1 , o2 , … , om
a1 ?
c ? a2 , … , an
? o2 , … , om
A partir de:
Se deduce:
Programación Lógica
Deducción progresiva o Hacia-Delante
Cuando se trata de una regla con un único antecedente, el resultado es la generación de un nuevo hecho
a1 ?
c ? a1
? a1 , o2 , … , om
a1 ?
c ?
? o2 , … , om
A partir de:
Se deduce:
Programación Lógica
Deducción progresiva o Hacia-Delante
El objetivo es llegar “al objetivo vacío”, es decir:
a1 ?
c ? a2 , … , an
?
A partir de:
Se deduce:
a1 ?
c ? a1 , a2 , … , an
? a1
Programación Lógica
Deducción progresiva o Hacia-Delante
El procedimiento consiste, en esencia, en generar nuevos hechos por reducción de los antecedentes de las reglas, y en reducir el objetivo, por aplicación de los hechos originales o los generados, hasta alcanzar el objetivo vacío, lo que equivale a haber satisfecho todos los subojetivos.
Programación Lógica
Deducción progresiva o Hacia-Delante
1. Formular el problema en términos de hechos, reglas y objetivos como cláusulas de Horn, y añadirlos a una base de datos inicialmente vacía.
2. Hasta que el objetivo esté vacío o no existan sustituciones aplicables.
2.1 Partiendo de algún hecho disponible, encontrar una regla con un antecedente, o un subobjetivo, que pueda ser sustituido, previa unificación, con el hecho en cuestión
2.2 Añadir a la base de datos, la siguiente regla o subobjetivo, donde ? es la unificación más general de la sustitución:
3. Si el objetivo está vacío, entonces el objetivo es cierto y las posibles respuestas vienen dadas por la secuencia de unificaciones. En otro caso, el objetivo no se puede verificar.
a1 ?
c ? a1 , a2 , … , an
? a1 , o2 , … , om
(c ? a2 , … , an) ?
(? o2 , … , om ) ?
Programación Lógica
Ejemplo:
Antonio y Miguel son dos amigos miembros de un club alpino. Cada miembro de este club que no es esquiador es escalador.
A los escaladores les disgusta la lluvia y, por otra parte, a los que les disgusta la nieve no son esquiadores.
Ambos amigos tienen gustos diferentes, de tal forma que a Miguel le disgusta los que a Antonio le gusta, y le gusta lo que a Antonio le disgusta.
A Antonio le gustan la nieve y la lluvia.
¿Existe algún miembro del club que sea escalador?. ¿Quién?.
Programación Lógica
Antonio y Miguel son dos amigos miembros de un club alpino. Cada miembro de este club que no es esquiador es escalador.
A los escaladores les disgusta la lluvia y,por otra parte,
a los que les disgusta la nieve no son esquiadores.
Ambos amigos tienen gustos diferentes, de tal forma que a Miguel le disgusta los que a Antonio le gusta,
y le gusta lo que a Antonio le disgusta.
A Antonio le gustan la nieve y la lluvia.
¿Existe algún miembro del club que sea escalador?. ¿Quién?.
escalador(X) ? no_esquiador(X)
disgusta(Y, lluvia) ? escalador(Y)
no_esquiador(Z) ? disgusta(Z, nieve)
disgusta(miguel, C) ? gusta(antonio, C)
gusta(miguel, A) ? disgusta(antonio, A)
gusta(antonio, lluvia) ?
gusta(antonio, nieve) ?
? escalador(Quien)
Programación Lógica
Partiendo de los dos únicos hechos iniciales, el proceso de deducción podría ser el siguiente:
gusta(antonio, lluvia) ?
{ C ? lluvia }
disgusta(miguel, lluvia) ?
escalador(X) ? no_esquiador(X)
disgusta(Y, lluvia) ? escalador(Y)
no_esquiador(Z) ? disgusta(Z, nieve)
disgusta(miguel, C) ? gusta(antonio, C)
gusta(miguel, A) ? disgusta(antonio, A)
gusta(antonio, lluvia) ?
gusta(antonio, nieve) ?
? escalador(Quien)
disgusta(miguel, C) ? gusta(antonio, C)
Programación Lógica
Partiendo de los dos únicos hechos iniciales, el proceso de deducción podría ser el siguiente:
gusta(antonio, nieve) ?
{ C ? nieve}
disgusta(miguel, nieve) ?
escalador(X) ? no_esquiador(X)
disgusta(Y, lluvia) ? escalador(Y)
no_esquiador(Z) ? disgusta(Z, nieve)
disgusta(miguel, C) ? gusta(antonio, C)
gusta(miguel, A) ? disgusta(antonio, A)
gusta(antonio, lluvia) ?
gusta(antonio, nieve) ?
? escalador(Quien)
disgusta(miguel, C) ? gusta(antonio, C)
no_esquiador(Z) ? disgusta(Z, nieve)
{ Z ? miguel}
no_esquiador(miguel) ?
escalador(X) ? no_esquiador(X)
{ X ? miguel}
escalador(miguel) ?
? escalador(Quien)
{ Quien ? miguel}
?
Conclusión: al menos un escalador, miguel
Programación Lógica
Deducción regresiva o Hacia-Atrás
Intuitivamente el procedimiento consiste en deducir el objetivo por aplicación sobre el mismo de las reglas y hechos.
Si existe algún subobjetivo a1 que pueda ser sustituido por un hecho, entonces el mismo está satisfecho:
a1 ?
? a1 , o2 , … , om
a1 ?
? o2 , … , om
A partir de:
Se deduce:
Programación Lógica
En caso contrario, y cuando el subobjetivo b puede ser sustituido por el consecuente de una regla, entonces el objetivo se modifica sustituyendo el subobjetivo por los antecedentes de la regla:
b ? a1 , a2 , …, an
? b , o2 , … , om
b ? a1 , a2 , …, an
? a1 , a2 , …, an , o2 , … , om
A partir de:
Se deduce:
Deducción regresiva o Hacia-Atrás
Programación Lógica
Deducción regresiva o Hacia-Atrás
En este último caso, el nuevo objetivo es más complejo al poseer más subobjetivos, pero se supone que cada uno de ellos es de menor complejidad, esto es, más cercanos a un hecho.
El resultado final se alcanza cuando se reduce al vacío el objetivo, lo que indicará que se han satisfecho todos los subobjetivos.
Programación Lógica
1. Formular el problema en términos de hechos, reglas y objetivos como cláusulas de Horn, y añadirlos a una base de datos inicialmente vacía.
2. Hasta que el objetivo esté vacío o no existan sustituciones aplicables.
2.1 Partiendo del objetivo, encontrar algún hecho o consecuente de regla que pueda que pueda ser sustituido, previa unificación, con algún subobjetivo
2.2 Añadir a la base de datos, el siguiente objetivo, donde ? es la unificación más general de la sustitución:
3. Si el objetivo está vacío, entonces el objetivo es cierto y las posibles respuestas vienen dadas por la secuencia de unificaciones. En otro caso, el objetivo no se puede verificar.
p ?
p ? a1 , a2 , … , an
? p , o2 , … , om
(? o2 , … , om ) ?
(? a1 , a2 , … , an , o2 , … , om ) ?
Deducción regresiva o Hacia-Atrás
Programación Lógica
Antonio y Miguel son dos amigos miembros de un club alpino. Cada miembro de este club que no es esquiador es escalador.
A los escaladores les disgusta la lluvia y,por otra parte,
a los que les disgusta la nieve no son esquiadores.
Ambos amigos tienen gustos diferentes, de tal forma que a Miguel le disgusta los que a Antonio le gusta,
y le gusta lo que a Antonio le disgusta.
A Antonio le gustan la nieve y la lluvia.
¿Existe algún miembro del club que sea escalador?. ¿Quién?.
escalador(X) ? no_esquiador(X)
disgusta(Y, lluvia) ? escalador(Y)
no_esquiador(Z) ? disgusta(Z, nieve)
disgusta(miguel, C) ? gusta(antonio, C)
gusta(miguel, A) ? disgusta(antonio, A)
gusta(antonio, lluvia) ?
gusta(antonio, nieve) ?
? escalador(Quien)
Programación Lógica
Partiendo del teorema:
escalador(Quien) ?
{ X ? Quien}
no_esquiador(Quien) ?
escalador(X) ? no_esquiador(X)
disgusta(Y, lluvia) ? escalador(Y)
no_esquiador(Z) ? disgusta(Z, nieve)
disgusta(miguel, C) ? gusta(antonio, C)
gusta(miguel, A) ? disgusta(antonio, A)
gusta(antonio, lluvia) ?
gusta(antonio, nieve) ?
? escalador(Quien)
disgusta(miguel, C) ? gusta(antonio, C)
no_esquiador(Z) ? disgusta(Z, nieve)
{ Z ? Quien}
disgusta(Quien, nieve) ?
escalador(X) ? no_esquiador(X)
{ Quien ? miguel,
C ? nieve }
gusta(antonio, nieve) ?
{ }
?
Conclusión: al menos un escalador, miguel
gusta(antonio, nieve) ?
Programación Lógica
En el proceso de exploración pueden producirse diversas situaciones anómalas como las siguientes
Bucles: Cuando la resolución de un objetivo conduce a que el mismo objetivo o alguno de sus sucesores se vuelva a plantear de nuevo como objetivo.
Desbordamientos: Cuando la resolución de un objetivo conduzca a un objetivo, que ni pueda ser reducido, ni presente condición de parada, es decir, que siempre existen reglas aplicables.
Duplicación de objetivos: Cuando se suscita la resolución de un objetivo ya resuelto con anterioridad.
Programación Lógica
Ejemplo de bucle debido a un problema mal definido.
rel(a, b) ?
rel(a, c) ?
alt(a, d) ?
rel(A, B) ? alt(A, B)
alt(X, Y) ? rel (a, Y)
? rel(a, D)
rel(a, D)
rel(a, b)
rel(a, c)
alt(a, D)
alt(a, d)
rel(a, D)
{D ? b}
{D ? c}
{A ? a
B ? D}
{D ? b}
{X ? a, Y ? D}
Programación Lógica
1rel(a, b) ?
2rel(a, c) ?
1alt(a, d) ?
3rel(A, B) ? alt(A, B)
2alt(X, Y) ? rel (a, Y)
? rel(a, D)
[rel(a, D)]
[1rel(a, D)] [2rel(a, D)] [3rel(a, D)]
{D ? b}
[1rel(a, b)] [2rel(a, D)] [3rel(a, D)]
[ ] [2rel(a, D)] [3rel(a, D)]
[2rel(a, D)] [3rel(a, D)]
{D ? c}
[2rel(a, c)] [3rel(a, D)]
[ ] [3rel(a, D)]
[3rel(a, D)]
{A ? a, B ? D}
[alt(a, D)]
[1alt(a, D)] [2alt(a, D)]
[1alt(a, D)] [2alt(a, D)]
{D ? d}
[1alt(a, d)] [2alt(a, D)]
[ ] [2alt(a, D)]
{X ? a, Y ? D }
[rel(a, D)]
Programación Lógica
Jack es dueño de un perro
Quien es dueño de un perro es un amante de los animales
Ningún amante de los animales mata a un animal
O Jack o Curiosidad mató al gato, cuyo nombre era Tuna
¿Mató Curiosidad al gato?
Programación Lógica
A. Jack es dueño de un perro
B. Quien es dueño de un perro es un amante de los animales
C. Ningún amante de los animales mata a un animal
D. O Jack o Curiosidad mató al gato, cuyo nombre era Tuna
E. ¿Mató Curiosidad al gato?
1. Expresión como predicados de primer orden
A. (?X) perro(X) ? dueño(jack, X)
B. (?X) {(?Y) perro(Y) ? dueño(X, Y)} ? naturalista(X)
C. (?X) (?Y) naturalista(X) ? animal(Y) ? ? mata(X,Y)
D1. mata(jack, tuna) ? mata(curiosidad, tuna)
D2. gato(tuna)
E. mata(curiosidad, tuna)
Es necesario añadir que los gatos son animales
F. (?X) gato(X) ? animal(X)
Programación Lógica
2. Transformación a cláusulas
Negación del teorema:
E. ? mata(curiosidad, tuna)
2.1 Eliminación de la implicaciones
B. (?X) {(?Y) perro(Y) ? dueño(X, Y)} ? naturalista(X)
C. (?X) (?Y) naturalista(X) ? animal(Y) ? ? mata(X,Y)
F. (?X) gato(X) ? animal(X)
B. (?X) ? {(?Y) perro(Y) ? dueño(X, Y)} ? naturalista(X)
C. (?X) (?Y) ? { naturalista(X) ? animal(Y)} ? ? mata(X,Y)
F. (?X) ? gato(X) ? animal(X)
Programación Lógica
2. Transformación a cláusulas
2.2 Mover las negaciones hasta las fórmulas atómicas
B. (?X) ? {(?Y) perro(Y) ? dueño(X, Y)} ? naturalista(X)
C. (?X) (?Y) ? { naturalista(X) ? animal(Y)} ? ? mata(X,Y)
B. (?X) {(?Y) ? perro(Y) ? ? dueño(X, Y)} ? naturalista(X)
C. (?X) (?Y) ? naturalista(X) ? ? animal(Y) ? ? mata(X,Y)
Programación Lógica
2. Transformación a cláusulas
2.3 Renombrar variables
A. (?X) perro(X) ? dueño(jack, X)
B. (?Y) {(?Z) ? perro(Z) ? ? dueño(Y, Z)} ? naturalista(Y)
C. (?U) (?W) ? naturalista(U) ? ? animal(W) ? ? mata(U,W)
F. (?C) ? gato(C) ? animal(C)
2.4 Eliminar los cuantificadores existenciales
A. (?X) perro(X) ? dueño(jack, X)
A. perro(a) ? dueño(jack, a)
donde a es una función de Skolem constante
Programación Lógica
2. Transformación a cláusulas
2.5 Desplazar los cuantificadores universales hasta el comienzo de las fórmulas
B. (?Y) {(?Z) ? perro(Z) ? ? dueño(Y, Z)} ? naturalista(Y)
B. (?Y) (?Z) ? perro(Z) ? ? dueño(Y, Z) ? naturalista(Y)
2.6 Convertir los operadores AND en los más externos
2.7 Eliminar los cuantificadores universales
2.8 Eliminar los conectores AND
Programación Lógica
2. Transformación a cláusulas
Conjunto de cláusulas resultante
A.1 perro(a)
A.2 dueño(jack,a)
B. ? perro(Z) ? ? dueño(Y, Z) ? naturalista(Y)
C. ? naturalista(U) ? ? animal(W) ? ? mata(U,W)
D1. mata(jack, tuna) ? mata(curiosidad, tuna)
D2. gato(tuna)
E. ? mata(curiosidad, tuna)
F. ? gato(C) ? animal(C)
Programación Lógica
3. Resolución por refutación
? mata(curiosidad, tuna)
mata(jack, tuna) ? mata(curiosidad, tuna)
mata(jack, tuna)
? naturalista(U) ? ? animal(W) ? ? mata(U,W)
? naturalista(jack) ? ? animal(tuna)
? perro(Z) ? ? dueño(Y, Z) ? naturalista(Y)
? perro(Z) ? ? dueño(jack, Z) ? ? animal(tuna)
dueño(jack, a)
? perro(a) ? ? animal(tuna)
? gato(C) ? animal(C)
? gato(tuna) ? ? perro(a)
gato(tuna)
? perro(a)
perro(a)
[ ]
{U ? jack, W? tuna}
{Y ? jack}
{Z ? a}
{C ? a}
Programación Lógica
Expresar como cláusulas de Horn:
A) caballos, vacas y cerdos son mamíferos
B) el hijo de un caballo es un caballo
C) “centella” es un caballo
D) “centella” es el padre de “chispas”
E) hijo y padre son relaciones inversas
F) todo mamífero tiene un padre
y, mediante deducción hacia atrás, contestar a la pregunta:
¿Cuántos caballos conocemos?
Programación Lógica
A) mamífero(X) ? vaca(X)
mamífero(Y) ? cerdo(Y)
mamífero(Z) ? caballo(Z)
B) caballo(centella) ?
C) caballo(W) ? caballo(U), hijo(W, U)
D) padre(centella, chispas) ?
E) padre(S, R) ? hijo(R, S)
hijo(P, Q) ? padre(Q, P)
F) padre(L, M) ? mamífero(M)
Programación Lógica
A) 1mamífero(X) ? vaca(X)
2mamífero(Y) ? cerdo(Y)
3mamífero(Z) ? caballo(Z)
B) 1caballo(centella) ?
C) 2caballo(W) ? caballo(U), hijo(W, U)
D) 1padre(centella, chispas) ?
E) 2padre(S, R) ? hijo(R, S)
hijo(P, Q) ? padre(Q, P)
F) 3padre(L, M) ? mamífero(M)
El objetivo: ? caballo(M)
Programación Lógica
[caballo(H)]
[1caballo(H)] [2caballo(H)] {H ? centella}
[caballo(centella)] [2caballo(H)]
[ ] [2caballo(H)] {W ? H}
[caballo(U), hijo(H,U)]
[1caballo(U), hijo(H,U)] [2caballo(U), hijo(H,U)] {U ? centella}
[caballo(centella), hijo(H, centella)] [2caballo(U), hijo(H,U)]
[hijo(H, centella)] [2caballo(U), hijo(H,U)] {P ? H, Q ? centella}
[padre(centella, H)] [2caballo(U), hijo(H,U)]
[1padre(centella, H)] [2padre(centella, H)]
[3padre(centella, H)] [2caballo(U), hijo(H,U)]
{H ? chispas}
[padre(centella, chispas)] [2padre(centella, H)]
[3padre(centella, H)] [2caballo(U), hijo(H,U)]
Programación Lógica
[ ] [2padre(centella, H)] [3padre(centella, H)] [2caballo(U), hijo(H,U)]
{S ? centella, R ? H}
[hijo(H, centella)] [3padre(centella, H)] [2caballo(U), hijo(H,U)]
{P ? H, Q ? centella}
[padre(centella, H)] [3padre(centella, H)] [2caballo(U), hijo(H,U)]
[1padre(centella, H)] [2padre(centella, H)]
[3padre(centella, H)]
[3padre(centella, H)] [2caballo(U), hijo(H,U)]
…
A partir de aquí sólo obtendremos una única respuesta H= chispas
Programación Lógica
¿Cuál sería ahora el resultado si cambiásemos el orden de las definiciones del predicado caballo?
A) 1mamífero(X) ? vaca(X)
2mamífero(Y) ? cerdo(Y)
3mamífero(Z) ? caballo(Z)
C) 2caballo(W) ? caballo(U), hijo(W, U)
B) 1caballo(centella) ?
D) 1padre(centella, chispas) ?
E) 2padre(S, R) ? hijo(R, S)
hijo(P, Q) ? padre(Q, P)
F) 3padre(L, M) ? mamífero(M)
El objetivo: ? caballo(M)
Programación Lógica
[caballo(H)]
[2caballo(H)] [1caballo(H)] {W ? H}
[caballo(U), hijo(H, U)][1caballo(centella)]
[2caballo(U), hijo(H, U)] [1caballo(U), hijo(H, U)][1caballo(H)]
{W ? U}
[caballo(F), hijo(U, F), hijo(H, U)] [1caballo(U), hijo(H, U)][1caballo(H)]
[2caballo(F), hijo(U, F), hijo(H, U)]
[1caballo(F), hijo(U, F), hijo(H, U)]
[1caballo(U), hijo(H, U)][1caballo(H)]
…
Y finalmente la pila se desbordaría
Programación Lógica
Supongamos ahora que intercambiamos el orden de las premisas de la regla C. ¿Qué pasaría?
A) 1mamífero(X) ? vaca(X)
2mamífero(Y) ? cerdo(Y)
3mamífero(Z) ? caballo(Z)
B) 1caballo(centella) ?
C) 2caballo(W) ? hijo(W, U), caballo(U).
D) 1padre(centella, chispas) ?
E) 2padre(S, R) ? hijo(R, S)
hijo(P, Q) ? padre(Q, P)
F) 3padre(L, M) ? mamífero(M)
El objetivo: ? caballo(M)
Programación Lógica
[caballo(H)]
[1caballo(H)] [2caballo(H)] {H ? centella}
[caballo(centella)] [2caballo(H)]
[ ] [2caballo(H)] {W ? H}
[hijo(H,U), caballo(U)] {P ? U, Q ? H}
[padre(U, H), caballo(U)]
[1padre(U, H), caballo(U)] [2padre(U, H), caballo(U)]
[3padre(U, H), caballo(U)]
{U ? centella, H ? chipas}
[1padre(centella, chispas), caballo(centella)] [2padre(U, H), caballo(U)]
[3padre(U, H), caballo(U)]
[caballo(centella)] [2padre(U, H), caballo(U)] [3padre(U, H), caballo(U)]
[1caballo(centella)] [2caballo(centella)]
[2padre(U, H), caballo(U)] [3padre(U, H), caballo(U)]
Programación Lógica
[1caballo(centella)] [2caballo(centella)]
[2padre(U, H), caballo(U)] [3padre(U, H), caballo(U)]
[ ] [2caballo(centella)]
[2padre(U, H), caballo(U)] [3padre(U, H), caballo(U)]
{W ? centella}
[hijo(centella, F), caballo(F)]
[2padre(U, H), caballo(U)] [3padre(U, H), caballo(U)]
…
Repetiríamos la misma demostración anterior, con otros
argumentos, y finalmente la pila se desbordaría
Programación Lógica
p(a, b) ?
p(a, X) ? r(X)
r(c) ?
r(d) ?
p(Y, Z) ? q(Y, Z)
q(a, e) ?
q(U, V) ? s(W), p(W, V)
s(a) ?
s(f) ?
? p(a, R)
Realizar la traza de la pila de demostración del teorema indicado
Programación Lógica
Problema. La función cons(X,Y) denota la lista formada insertando X en la cabeza de la lista Y. Así podemos representar la lista vacía por nil; la lista (2) por cons(2, nil); la lista (1,2) por cons(1, cons(2, nil)); y así sucesivamente. La formula last(lista, ultimo) devuelve en ultimo el último elemento de la lista “lista”. Supongamos los siguientes axiomas:
(? U) [last(cons(U, nil), U)]
(? X, Y, Z) [last(Y, Z) ? last(cons(X, Y), Z)]
Probar por resolución por refutación el siguiente teorema:
(? V) [last(cons(2, cons(1, nil)), V)]
Emplear el método de obtención de respuestas para encontrar el valor de V, el último elemento de la lista (1,2).
Programación Lógica
Bibliografía.
[Mend-92] J. Méndez
Apuntes del Curso de I.A.
U.L.P.G.C.
[Nils-82] N. J. Nilsson
Principles of Artificial Intelligence
Springer-Verlag, 1982.
[Apt-97] K.R. Apt,
From Logic Programming to Prolog
Prentice-Hall, 1997.
[Nils-98 ] N. J. Nilsson
Artificial Intelligence
Morgan Kaufmann, 1998.
 Página anterior | Volver al principio del trabajo | Página siguiente  |