Source: https://www.slideshare.net/FernandoCaparrini/logica-15868035
Timestamp: 2017-08-22 17:41:41+00:00

Document:
Jflambert lyada -ayudantia 1 prolog by Francisco Lambert... 1267 views
Grafos 0 by brisarosales 889 views
Fbf by UNAD - Universida... 1992 views
Pero… ¿qué es la Constitución Polít... by hargar1 49 views
Concepto epistemologico by Rodolfo Hidalgo 8333 views
Epistemología ii by secretaria 4311 views
Es muy buena, ¿la puede compartir?
1. Introducción a laProgramación Lógica
2. Objetivo: • Presentar la Lógica de Primer Orden (LPO) como método formal de representación del conocimiento e inferencia. • Estudiar los métodos de inferencia automáticos aplicables a la LPO (en concreto, el método de resolución por refutación).
3. Representación e inferencia en LPOIdea: La lógica como sistema de representación del conocimiento y de obtención de consecuenciasCálculo en LPO Fórmulas atómicas Fórmulas Conectores
4. Fórmulas atómicas Términos autor(quijote, cervantes) escritor(cervantes) autor(quijote, Quién) autor(quijote, mejor(novelista, españa)) Predicado: Un predicado es un símbolo cuyo valor se encuentra en el dominio lógico (verdadero o falso) y representa alguna cualidad semántica, en un cierto contexto, acerca de las relaciones entre objetos o entidades
5. Conectores Permiten construir fórmulas complejas a partir de fórmulas o expresiones más sencillas: Negación : ¬ Disyunción : ∨ (or) Conjunción : ∧ (and) Implicación : → Equivalencia : ↔
6. Negación: Genera una fórmula que posee valores lógicoscontrarios a los de la fórmula sobre la que se aplica.Estrictamente no es un conector, pues no conecta dosfórmulas sino que transforma una. ¬ autor(hamlet, cervantes)Disyunción: Genera una fórmula que es cierta si algunade las que conecta es cierta.estado(bombilla, encendida) ∨ estado(bombilla, apagada)Conjunción: Genera una fórmula que es cierta si las osfórmulas que conecta son ciertas. color(coche, rojo) ∧ color(camisa, azul)
7. Implicación: Genera una fórmula que es cierta siempresalvo cuando el antecedente es cierto y el consecuentefalso. p → q es equivalente a ¬p ∨ q p q p→q ¬p ¬p ∨ q 0 0 1 1 1 0 1 1 1 1 1 0 0 0 0 1 1 1 0 1 está(cielo, azul) → ¬ lloverá(hoy) ¬ está(cielo, azul) ∨ ¬ lloverá(hoy)
8. Equivalencia o doble implicación: Genera una fórmulaque es cierta sólo si las dos componentes poseen elmismo valor. p ↔ q es equivalente a (p → q) ∧ (q → p) p q p→q q→p (p → q) ∧ (q → p) 0 0 1 1 1 0 1 1 0 0 1 0 0 1 0 1 1 1 1 1 llueve(hoy) ↔ está(cielo, nublado)
9. EquivalenciasComplemento: p∨¬p≡1Doble negación: ¬(¬p)≡pConmutativa: p∨q≡q∨p p∧q≡q∧pDistributiva: p ∨ (q ∧ r) ≡ (p ∨ q) ∧ (p ∨ r) p ∧ (q ∨ r) ≡ (p ∧ q) ∨ (p ∧ r)Asociativa: p ∨ (q ∨ r) ≡ (p ∨ q) ∨ r p ∧ (q ∧ r) ≡ (p ∧ q) ∧ rLeyes de De Morgan: ¬ (p ∨ q) ≡ ¬ p ∧ ¬ q ¬ (p ∧ q) ≡ ¬ p ∨ ¬ qLey del contrapositivo: p→q≡¬q→¬p
10. Establecen el ámbito deCuantificadores existencia de las variablesCuantificador Universal (∀): Establece que la fórmula es siempre válida para cada valor posible de la variable X. La variable X se dice entonces cuantificada universalmente. “Todo cuerpo con masa cae” ∀X ( [cuerpo(X) ∧ posee(X,masa)] → cae(X) )Cuantificador Existencial (∃): Establece que como mínimo existe un valor de la variable cuantificada que hace cierta la fórmula. La variable se dice cuantificada existencialmente. “Alguien descubrió la penicilina” ∃ X ( descubrió( X, penicilina )
11. Reglas de precedencia entre operadores ¬ ∀, ∃ menor precedencia ∨,∧ →, ↔
12. Forma Prenex de una fórmulaUna fórmula se dice que está en forma prenex si todos loscuantificadores se encuentran al principio de la fórmula.Algunas equivalencias útiles para alcanzar una formanormal ¬ [ ∃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) ]
13. Reglas de InferenciaEspecialización Universal: siempre es posible deducir la verificación deun caso concreto a partir de un cuantificador universal. ∀X p(X) ⇒ p(a)Sustitución: permite la sustitución de cualquier proposición en unafórmula por otra equivalente.Modus ponens: Axioma: p → q Axioma: p Teorema: qModus tollens: Axioma: p → q Axioma: ¬q Teorema: ¬p∧ Introducción: p∧q puede ser inferida de p y q.∧ Eliminación: p puede ser inferida de p∧q.∨ Introducción: p ∨ q puede ser inferida de p o de q.
14. Lo que queremos hacer ...Teorema + Axiomas +Teorema + Axiomas (como cláusulas) +Método de resolución por refutación UnificaciónDemostración automática de teoremas
15. IMPORTANTE:La demostración automática de teoremas lógicos es unprocedimiento que involucra una mera actividadsintáctica, o de relación entre símbolos, ignorándosecompletamente el contenido semántico que resulta dela interpretación de las fórmulas.
16. 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
17. Cláusulas de Horn.Aquellas cuyo consecuente tiene un único predicado. a1 ∧ a2 ∧ ... ∧ an → bVentajas de una representación basada en cláusulas deHorn• La demostración de teoremas o resolución de un conjuntode cláusulas de Horn es más sencilla en general.• Las cláusulas de Horn admiten una interpretación directaen términos de un lenguaje de programación, lo que no esposible con cláusulas generales.
18. Transformación a cláusulasPara ilustrar el proceso paso a paso emplearemos lasiguiente 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 → qpor ¬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)]}}
19. 2. Mover las negaciones hasta las fórmulas atómicas, paraello se emplean las leyes de Morgan y las transformacionesde 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)]}}
20. 3. Renombrar variables, en aquellos casos en los que variasvariables se hayan nombrado de igual forma. En nuestrocaso esto ocurre con la variable Y que renombramos como Zen 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)]}}
21. 4. Eliminar los cuantificadores existenciales. Las variablescuantificadas por este tipo de cuantificadores seránsustituidas por un tipo de función comodín denominadafunció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 cuantificadoresexistenciales sino también las variables ligadas a los mismos.La función de Skolem introducida debe ser nueva en eluniverso de discurso, y además deberá ser función de todaslas variables cuantificadas universalmente cuyos ámbitosincluyan el ámbito del cuantificador existencial que sepretende eliminar.
22. 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 deningún cuantificador universal, se usará una función deSkolem 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 quesabemos existe. Evidentemente a debe ser un símbolo queno haya sido empeado con anterioridad.
23. 5. Desplazar los cuantificadores universales, de manera quequeden al comienzo de la fórmula (forma prenex. Estreproceso puede ser realizado por cuanto no existen yavariables 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 en los más externos,para lo que se emplean las leyes distributivas. A la formaresultante se le denomina forma normal conjuntiva.Este paso se ejecuta sobre el ejemplo en dos pasos:
24. 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))]}
25. 7. Eliminar los cuantificadores universales. Se trata deuna eliminación convencional, no teórica, pues se asumeque toda variable que aparezca está cuantificadauniversalmente. La función de Skolem adquiere sentido,dado que al no aparecer otras variables que lasuniversales, pueden eliminarse sus cuantificadores porconvenio. 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))]
26. 8. Eliminar los conectores conjuntivos.Dado que la fómula se corresponde con una conjunciónde subfómulas, éstas deberán verificarse por separadopara que se verifique la fórmula principal.Esto produce, en nuestro caso, el siguiente conjunto defó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))
27. 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 LPO.
28. Unificación y sustituciónUn proceso de unificación puede ser representado mediante unoperador θ constituido por un conjunto de pares de términosordenados por: θ = { v1→ t1, v2→ t2, ..., vn→ tn}donde el par vi→ ti, indica que la variable vi es sustituida por elté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}
29. 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) θ1 = { X → g(Z), Y → a } P2: p(X, f(a), b) θ2 = { Y → a } P3: p(Z, f(U), b) θ3 = { X → Z, Y → U } P4: p(c, f(a), b) θ4 = { X → c, Y → a }
30. Resolución por refutación Si queremos demostrar un teorema dado en base a unconjunto de axiomas que suponemos consistente, podemoshacerlo mostrando que el conjunto formado por la negacióndel teorema y el conjunto de axiomas es inconsistente.Si tal inconsistencia se demuestra será porque el teoremaera cierto. Un sistema lógico se dice inconsistente si dos expresiones V y ¬V son simultáneamente válidas en él. 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.
31. Decidibilidad y ConsistenciaSi A es un conjunto de cláusulas lógicas consistentes,denominadas Axiomas, y T es otra cláusula, denominadaTeorema, entonces si T es una consecuencia lógica de Ase debe verificar:1. El conjunto A ∪ T es consistente2. El conjunto A ∪ ¬T es inconsistenteSólo la segunda propiedad es verificable de forma efectiva,de donde se deduce intuitivamente un procedimiento dedemostración de teoremas que consiste en demostrar lainconsistencia de A ∪ ¬T . A este procedimiento se ledenomina de Resolución por Refutación del Teorema.
32. Cláusula resolventeSean dos cláusulas, que denominaremos cláusulas padres, quecontengan respectivamente, una misma proposición, negada y sinnegar, cada una de ellas. Como es el caso de la proposición p 1 en elsiguiente ejemplo: p1 v p2 v ... v pn ¬ p1 v q2 v ... v qmAmbas cláusulas forman parte de un sistema que se asume consistentey, por tanto, son ciertas. Puede construirse entonces una nuevacláusula, denominada cláusula resolvente a partir de la disyunción deambas 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
33. Cláusula resolventeLa nueva cláusula (cláusula resolvente) debe ser cierta por cuanto lascláusulas padre forman un conjunto de cláusulas consistente con lo queel conjunto que resulta de añadir la cláusula resolvente al conjunto decláusulas anterior sigue siendo consistente.Los siguientes son algunos ejemplos de la aplicación del método de laclá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) ≡¬pvr (encadenamiento de reglas)(p v ¬ q) v (¬ p v q) ≡qv¬q (tautología)Nótese que en el último caso, también podría resolverse sobre q yobtendríamos como cláusula resolvente p v ¬ p. Lo que no es correctoes resolver doblemente sobre p y q y obtener un resolvente nulo.
34. Cláusula resolvente(p v ¬ q) v (¬ p v q) ≡qv¬q (tautología)Una forma de ver que la doble resolución es un error es considerar elcaso sencillo anterior cuando se resuelve doblemente. En ese casoobtendríamos la cláusula nula, indicando una inconsistencia. Sinembargo, podemos comprobar que ambas cláusulas son consistentescuando ambos predicados son verdaderos, lo que indica que laconclusión de inconsistencia que se deriva de la doble resolución esincorrecta.La idea que subyace en el método de resolución se basa en que lafórmula ((p v α) ∧ (¬ p v β)) → (α v β) es una tautología (demostrarloempleando una tabla de verdad).Por el contrario, puede comprobarse que la fórmula similar que deberíasustentar la doble resolución, ((p v r v α) ∧ (¬ p v ¬ r v β)) → (α v β) ,donde r es q o ¬ q, no es válida.
35. Resolución por RefutaciónLa resolución por refutación consiste esencialmente en aplicar elmétodo de la cláusula resolvente para eventualmente alcanzar elresolvente nulo. Si esto es posible se habrá demostrado lainconsistencia del conjunto formado por los axiomas (cuya validez estágarantizada) y el teorema negado, en cuyo caso el teorema seconsidera demostrado. ¬avb ¬bvc a ¬c ¬avc c nil
36. Resolución por RefutaciónPara poder aplicar el método de la cláusula resolvente a predicados yno sólo a proposiciones es preciso primeramente unificar las cláusulaspara conseguir que los términos de los predicados complementariossean 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 comopredicados 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)
37. Resolución por RefutaciónOtra forma de generar una cláusula resolvente más sencilla consiste eneliminar alguna de las realizaciones del mismo predicado p en algunade las cláusulas padre. Por ejemplo, encontrando un unificador yabsorbiendo 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 comoresolvente: q(a) ∨ ¬ q(X)
38. Resolución por RefutaciónUna 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.
39. Resolución por RefutaciónIdea 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.
40. Algoritmo: Resolución por Refutación0. Se supone que tanto los axiomas como la negación del teoremahan sido transformados en cláusulas.1. Incluir en el conjunto de cláusulas TRABAJO el conjunto deaxiomas y el teorema negado.2. Repetir hasta que se produzca la cláusula nula, o no se encuentreningú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 casocontrario, el teorema se supone falso.
41. Ejemplo: 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))
42. Ejemplo: Paso a cláusulas Axiomas A.1 ∀X(r(X) → l(X)) ¬ r(X) ∨ l(X) A.2 ∀X(d(X) → ¬ l(X)) ¬ d(Y) ∨ ¬ l(Y) A.3 ∃X(d(X) ∧ i(X)) d(a) i(a) Teorema. T. ∃X(i(X) ∧ ¬ r(X)) ¬ i(Z) ∨ r(Z) donde a es una constante de Skolem
43. Ejemplo: Grafo de resolución ¬ i(Z) ∨ r(Z) i(a) {Z→ a} r(a) ¬ r(X) ∨ l(X) {X→ a}¬ d(Y) ∨ ¬ l(Y) l(a) {Y→ a} ¬ d(a) d(a) {}
44. El proceso de resolución puede simplificarse si ,previamente o durante el proceso se realizan determinadaseliminaciones 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 quepuedan 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} absorbea 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 serevaluado (debido a mecanismos extralógicos o de tipo procedimental)y se evalúa a cierto entonces es posible eliminar la cláusula que locontiene. Si se evalúa a falso, entonces simplemente se puedeeliminar ese predicado de la cláusula.
45. 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.
46. 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.
47. 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
48. 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
49. Deducción progresiva o Hacia-Delante1. Formular el problema en términos de hechos, reglas y objetivos comoclá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 a1 ← c ← a1 , a2 , ... , an ← a1 , o2 , ... , om 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: (c ← a2 , ... , an) θ (← o2 , ... , om ) θ3. Si el objetivo está vacío, entonces el objetivo es cierto y las posiblesrespuestas vienen dadas por la secuencia de unificaciones. En otrocaso, el objetivo no se puede verificar.
50. Deducción regresiva o Hacia-Atrás1. Formular el problema en términos de hechos, reglas y objetivos comoclá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 p← p ← a1 , a2 , ... , an ← p , o2 , ... , om 2.2 Añadir a la base de datos, el siguiente objetivo, donde θ es la unificación más general de la sustitución: (← o2 , ... , om ) θ (← a1 , a2 , ... , an , o2 , ... , om ) θ3. Si el objetivo está vacío, entonces el objetivo es cierto y las posiblesrespuestas vienen dadas por la secuencia de unificaciones. En otrocaso, el objetivo no se puede verificar.

References: resolución 
 resolución 
 resolución 
 Resolución 
 Resolución 
 resolución 
 resolución 
 resolución 
 Resolución 
 resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 Resolución 
 resolución 
 resolución