Source: https://www.slideshare.net/JoseAAlonso/lmft5-resolucin-proposicional
Timestamp: 2018-04-22 15:43:27+00:00

Document:
I1M2010-T23: Técnicas de diseño des... by José A. Alonso 1359 views
I1M2010-T20: El tipo abstracto de l... by José A. Alonso 629 views
I1M-T19: El TAD de los árboles de b... by José A. Alonso 325 views
DAO2011-T0: Presentación de sistema... by José A. Alonso 1202 views
LMF-T4: Formas normales by José A. Alonso 1515 views
I1M-T21: El TAD de los polinomios e... by José A. Alonso 930 views
1. LMF Tema 5: Resolución proposicional Lógica matemática y fundamentos (2011–12) Tema 5: Resolución proposicional 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 / 37
2. LMF Tema 5: Resolución proposicionalTema 5: Resolución proposicional 1. Lógica de cláusulas 2. Demostraciones por resolución 3. Algoritmos de resolución 4. Reﬁnamientos de resolución 5. Argumentación por resolución 2 / 37
3. LMF Tema 5: Resolución proposicional Lógica de cláusulasTema 5: Resolución proposicional 1. Lógica de cláusulas Sintaxis de la lógica clausal Semántica de la lógica clausal Equivalencias entre cláusulas y fórmulas Modelos, consistencia y consecuencia entre cláusulas Reducción de consecuencia a inconsistencia de cláusulas 2. Demostraciones por resolución 3. Algoritmos de resolución 4. Reﬁnamientos de resolución 3 / 37
4. LMF Tema 5: Resolución proposicional Lógica de cláusulas Sintaxis de la lógica clausalSintaxis de la lógica clausal Un átomo es una variable proposicional. Variables sobre átomos: p, q, r , . . . , p1 , p2 , . . .. Un literal es un átomo (p) o la negación de un átomo (¬p). Variables sobre literales: L, L1 , L2 , . . .. Una cláusula es un conjunto ﬁnito de literales. Variables sobre cláusulas: C , C1 , C2 , . . .. La cláusula vacía es el conjunto vacío de literales. La cláusula vacía se representa por . Conjuntos ﬁnitos de cláusulas. Variables sobre conjuntos ﬁnitos de cláusulas: S, S1 , S2 , . . .. 4 / 37
5. LMF Tema 5: Resolución proposicional Lógica de cláusulas Semántica de la lógica clausalSemántica de la lógica clausal Una interpretación es una aplicación I : VP → B. El valor de un literal positivo p en una interpretación I es I(p). El valor de un literal negativo ¬p en una interpretación I es 1, si I(p) = 0; I(¬p) = 0, si I(p) = 1. El valor de una cláusula C en una interpretación I es 1, si existe un L ∈ C tal que I(L) = 1; I(C ) = 0, en caso contrario. El valor de un conjunto de cláusulas S en una interpretación I es 1, si para toda C ∈ S, I(C ) = 1 I(S) = 0, en caso contrario. Prop.: En cualquier interpretación I, I( ) = 0. 5 / 37
6. LMF Tema 5: Resolución proposicional Lógica de cláusulas Equivalencias entre cláusulas y fórmulasCláusulas y fórmulas Equivalencias entre cláusulas y fórmulas Def.: Una cláusula C y una fórmula F son equivalentes si I(C ) = I(F ) para cualquier interpretación I. Def.: Un conjunto de cláusulas S y una fórmula F son equivalentes si I(S) = I(F ) para cualquier interpretación I. Def.: Un conjunto de cláusulas S y un conjunto de fórmulas {F1 , . . . , Fn } son equivalentes si, para cualquier interpretación I, I(S) = 1 syss I es un modelo de {F1 , . . . , Fn }. De cláusulas a fórmulas Prop.: La cláusula {L1 , L2 , . . . , Ln } es equivalente a la fórmula L1 ∨ L2 ∨ · · · ∨ Ln . Prop.: El conjunto de cláusulas {{L1,1 , . . . , L1,n1 }, . . . , {Lm,1 , . . . , Lm,nm }} es equivalente a la fórmula (L1,1 ∨ · · · ∨ L1,n1 ) ∧ · · · ∧ (Lm,1 ∨ · · · ∨ Lm,nm ). 6 / 37
7. LMF Tema 5: Resolución proposicional Lógica de cláusulas Equivalencias entre cláusulas y fórmulasDe fórmulas a cláusulas (forma clausal) Def.: Una forma clausal de una fórmula F es un conjunto de cláusulas equivalente a F . Prop.: Si (L1,1 ∨ · · · ∨ L1,n1 ) ∧ · · · ∧ (Lm,1 ∨ · · · ∨ Lm,nm ) es una forma normal conjuntiva de la fórmula F . Entonces, una forma clausal de F es {{L1,1 , . . . , L1,n1 }, . . . , {Lm,1 , . . . , Lm,nm }}. Ejemplos: Una forma clausal de ¬(p ∧ (q → r )) es {{¬p, q}, {¬p, ¬r }}. Una forma clausal de p → q es {{¬p, q}}. El conjunto {{¬p, q}, {r }} es una forma clausal de las fórmulas (p → q) ∧ r y ¬¬r ∧ (¬q → ¬p). Def.: Una forma clausal de un conjunto de fórmulas S es un conjunto de cláusulas equivalente a S. Prop.: Si S1 , . . . , Sn son formas clausales de F1 , . . . , Fn , entonces S1 ∪ · · · ∪ Sn es una forma clausal de {F1 , . . . , Fn }. 7 / 37
8. LMF Tema 5: Resolución proposicional Lógica de cláusulas Modelos, consistencia y consecuencia entre cláusulasModelos, consistencia y consecuencia entre cláusulas Def.: Una interpretación I es modelo de un conjunto de cláusulas S si I(S) = 1. Ej.: La interpretación I tal que I(p) = I(q) = 1 es un modelo de {{¬p, q}, {p, ¬q}}. Def.: Un conjunto de cláusulas es consistente si tiene modelos e inconsistente, en caso contrario. Ejemplos: {{¬p, q}, {p, ¬q}} es consistente. {{¬p, q}, {p, ¬q}, {p, q}, {¬p, ¬q}} es inconsistente. Prop.: Si ∈ S, entonces S es inconsistente. Def.: S |= C si para todo modelo I de S, I(C ) = 1. 8 / 37
9. LMF Tema 5: Resolución proposicional Lógica de cláusulas Reducción de consecuencia a inconsistencia de cláusulasReducción de consecuencia a inconsistencia de cláusulas Prop: Sean S1 , . . . , Sn formas clausales de las fórmulas F 1 , . . . , Fn . {F1 , . . . , Fn } es consistente syss S1 ∪ · · · ∪ Sn es consistente. Si S es una forma clausal de ¬G, entonces son equivalentes 1. {F1 , . . . , Fn } |= G. 2. {F1 , . . . , Fn ¬G} es inconsistente. 3. S1 ∪ · · · ∪ Sn ∪ S es inconsistente. Ejemplo: {p → q, q → r } |= p → r syss {{¬p, q}, {¬q, r }, {p}, {¬r }} es inconsistente. 9 / 37
10. LMF Tema 5: Resolución proposicional Demostraciones por resoluciónTema 5: Resolución proposicional 1. Lógica de cláusulas 2. Demostraciones por resolución Regla de resolución proposicional Demostraciones por resolución 3. Algoritmos de resolución 4. Reﬁnamientos de resolución 5. Argumentación por resolución 10 / 37
11. LMF Tema 5: Resolución proposicional Demostraciones por resolución Regla de resolución proposicionalRegla de resolución Reglas habituales: p → q, p {¬p, q}, {p} Modus Ponens: q {q} p → q, ¬q {¬p, q}, {¬q} Modus Tollens: ¬p {¬p} p → q, q → r {¬p, q}, {¬q, r } Encadenamiento: p→r {¬p, r } Regla de resolución proposicional: {p1 , . . . , r , . . . , pm }, {q1 , . . . , ¬r , . . . , qn } {p1 , . . . , pm , q1 , , . . . , qn } 11 / 37
12. LMF Tema 5: Resolución proposicional Demostraciones por resolución Regla de resolución proposicionalRegla de resolución Def.: Sean C1 una cláusula, L un literal de C1 y C2 una cláusula que contiene el complementario de L. La resolvente de C1 y C2 respecto de L es ResL (C1 , C2 ) = (C1 {L}) ∪ (C2 {Lc }) Ejemplos: Resq ({p, q}, {¬q, r }) = {p, r } Resq ({q, ¬p}, {p, ¬q}) = {p, ¬p} Resp ({q, ¬p}, {p, ¬q}) = {q, ¬q} Resp ({q, ¬p}, {q, p}) = {q} Resp ({p}, {¬p}) = Def.: Res(C1 , C2 ) es el conjunto de las resolventes entre C1 y C2 Ejemplos: Res({¬p, q}, {p, ¬q}) = {{p, ¬p}, {q, ¬q}} Res({¬p, q}, {p, q}) = {{q}} Res({¬p, q}, {q, r }) =∅ Nota: ∈ Res({p, q}, {¬p, ¬q}) 12 / 37
13. LMF Tema 5: Resolución proposicional Demostraciones por resolución Demostraciones por resoluciónEjemplo de refutación por resolución Refutación de {{p, q}, {¬p, q}, {p, ¬q}, {¬p, ¬q}} : 1 {p, q} Hipótesis 2 {¬p, q} Hipótesis 3 {p, ¬q} Hipótesis 4 {¬p, ¬q} Hipótesis 5 {q} Resolvente de 1 y 2 6 {¬q} Resolvente de 3 y 4 7 Resolvente de 5 y 6 13 / 37
14. LMF Tema 5: Resolución proposicional Demostraciones por resolución Demostraciones por resoluciónEjemplo de grafo de refutación por resolución Grafo de refutación de {{p, q}, {¬p, q}, {p, ¬q}, {¬p, ¬q}} : 14 / 37
15. LMF Tema 5: Resolución proposicional Demostraciones por resolución Demostraciones por resoluciónDemostraciones por resolución entre cláusulas Sea S un conjunto de cláusulas. La sucesión (C1 , . . . , Cn ) es una demostración por resolución de la cláusula C a partir de S si C = Cn y para todo i ∈ {1, ..., n} se veriﬁca una de las siguientes condiciones: Ci ∈ S; existen j, k < i tales que Ci es una resolvente de Cj y Ck La cláusula C es demostrable por resolución a partir de S si existe una demostración por resolución de C a partir de S. Se representa por S Res C Una refutación por resolución de S es una demostración por resolución de la cláusula vacía a partir de S. Se dice que S es refutable por resolución si existe una refutación por resolución a partir de S. Se representa por S Res 15 / 37
16. LMF Tema 5: Resolución proposicional Demostraciones por resolución Demostraciones por resoluciónDemostraciones por resolución entre fórmulas Def.: Sean S1 , . . . , Sn formas clausales de las fórmulas F1 , . . . , Fn y S una forma clausal de ¬F Una demostración por resolución de F a partir de {F1 , . . . , Fn } es una refutación por resolución de S1 ∪ · · · ∪ Sn ∪ S. Def.: La fórmula F es demostrable por resolución a partir de {F1 , . . . , Fn } si existe una demostración por resolución de F a partir de {F1 , . . . , Fn }. Se representa por {F1 , . . . , Fn } Res F . Ejemplo: {p ∨ q, p ↔ q} Res p ∧ q 1 {p, q} Hipótesis 2 {¬p, q} Hipótesis 3 {p, ¬q} Hipótesis 4 {¬p, ¬q} Hipótesis 5 {q} Resolvente de 1 y 2 6 {¬q} Resolvente de 3 y 4 7 Resolvente de 5 y 6 16 / 37
17. LMF Tema 5: Resolución proposicional Demostraciones por resolución Demostraciones por resoluciónAdecuación y completitud de la resolución Prop.: Si C es una resolvente de C1 y C2 , entonces {C1 , C2 } |= C . Prop.: Si ∈ S, entonces S es inconsistente. Prop.: Sea S un conjunto de cláusulas. (Adecuación) Si S Res , entonces S es inconsistente. (Completitud) Si S es inconsistente, entonces S Res . Prop.: Sean S un conjunto de fórmulas y F es una fórmula. (Adecuación) Si S Res F , entonces S |= F . (Completitud) Si S |= F , entonces S Res F . Nota: Sean C1 y C2 las cláusulas {p} y {p, q}, respectivamente. Entonces, {C1 } |= C2 . C2 no es demostrable por resolución a partir de {C1 }. La fórmula de forma clausal C1 es F1 = p. La fórmula de forma clausal C2 es F2 = p ∨ q. {F1 } Res F2 . 17 / 37
18. LMF Tema 5: Resolución proposicional Algoritmos de resoluciónTema 5: Resolución proposicional 1. Lógica de cláusulas 2. Demostraciones por resolución 3. Algoritmos de resolución Algoritmo de resolución por saturación Algoritmo de saturación con simpliﬁcación 4. Reﬁnamientos de resolución 5. Argumentación por resolución 18 / 37
19. LMF Tema 5: Resolución proposicional Algoritmos de resolución Algoritmo de resolución por saturaciónAlgoritmo de de resolución por saturación Def.: Sea S un conjunto de cláusulas. Res(S) = S ∪ ( {Res(C1 , C2 ) : C1 , C2 ∈ S}). Algoritmo de resolución por saturación Entrada: Un conjunto ﬁnito de cláusulas, S. Salida: Consistente, si S es consistente; Inconsistente, en caso contrario. S := ∅ mientras ( ∈ S) y (S = S ) hacer S := S S := Res(S) fmientras si ( ∈ S) entonces Devolver Inconsistente en caso contrario Devolver Consistente fsi Prop.: El algoritmo de resolución por saturación es correcto. 19 / 37
20. LMF Tema 5: Resolución proposicional Algoritmos de resolución Algoritmo de resolución por saturaciónEjemplo de grafo de resolución por saturación Grafo de {{p, q}, {¬p, q}, {p, ¬q}, {¬p, ¬q}} : Traza: Paso S S 0 {1, 2, 3, 4} ∅ 1 {1, 2, 3, 4, 5, 6, 7, 8, 9, 10} {1, 2, 3, 4} 2 {1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11} {1, 2, 3, 4, 5, 6, 7, 8, 9, 10} 20 / 37
21. LMF Tema 5: Resolución proposicional Algoritmos de resolución Algoritmo de saturación con simpliﬁcaciónAlgoritmo de saturación con simpliﬁcación Prop.: Si S1 ⊆ S2 y S2 es consistente, entonces S1 es consistente. Prop.: Una cláusula es una tautología syss contiene un literal y su complementario. Prop.: Sea C ∈ S una tautología. Entonces S es consistente syss S {C } es consistente. Def.: La cláusula C subsume a la cláusula D si C ⊂ D (es decir, C ⊆ D y C = D). Prop.: Si C subsume a D, entonces C |= D. Prop.: Sean C , D ∈ S tales que C subsume a D. Entonces S es consistente syss S {D} es consistente. Def.: El simpliﬁcado de un conjunto ﬁnito de cláusulas S es el conjunto obtenido de S suprimiendo las tautologías y las cláusulas subsumidas por otras; es decir, Simp(S) = S − {C ∈ S : (C es una tautología) ó (existe D ∈ S tal que D ⊂ C )} 21 / 37
22. LMF Tema 5: Resolución proposicional Algoritmos de resolución Algoritmo de saturación con simpliﬁcaciónAlgoritmo de saturación con simpliﬁcación Algoritmo de resolución por saturación con simpliﬁcación: Entrada: Un conjunto ﬁnito de cláusulas, S. Salida: Consistente, si S es consistente; Inconsistente, en caso contrario. S := ∅ mientras ( ∈ S) y (S = S ) hacer S := S S := Simp(Res(S)) fmientras si ( ∈ S) entonces Devolver Inconsistente en caso contrario Devolver Consistente fsi Prop.: El algoritmo de resolución por saturación con simpliﬁcación es correcto. 22 / 37
23. LMF Tema 5: Resolución proposicional Algoritmos de resolución Algoritmo de saturación con simpliﬁcaciónGrafo de resolución por saturación con simpliﬁcación Resolución de {{p, q}, {¬p, q}, {p, ¬q}, {¬p, ¬q}} : Traza: Paso S S 0 {1, 2, 3, 4} ∅ 1 {5, 6, 7, 8} {1, 2, 3, 4} 2 {9} {5, 6, 7, 8} 23 / 37
24. LMF Tema 5: Resolución proposicional Algoritmos de resolución Algoritmo de saturación con simpliﬁcaciónGrafo de resolución por saturación con simpliﬁcación Resolución de {{p}, {¬p, q}, {¬q, ¬r }} : Traza: Paso S S 0 {1, 2, 3} ∅ 1 {1, 3, 4, 5} {1, 2, 3} 2 {1, 4, 6} {1, 3, 4, 5} 3 {1, 4, 6} {1, 4, 5, 6} Modelo: I(p) = 1, I(q) = 1, I(r ) = 0. 24 / 37
25. LMF Tema 5: Resolución proposicional Reﬁnamientos de resoluciónTema 5: Resolución proposicional 1. Lógica de cláusulas 2. Demostraciones por resolución 3. Algoritmos de resolución 4. Reﬁnamientos de resolución Resolución positiva Resolución negativa Resolución unitaria Resolución por entradas Resolución lineal 25 / 37
26. LMF Tema 5: Resolución proposicional Reﬁnamientos de resolución Resolución positivaResolución positiva Def.: Un literal positivo es un átomo. Def.: Una cláusula positiva es un conjunto de literales positivos. Def.: Una demostración por resolución positiva es una demostración por resolución en la que en cada resolvente interviene una cláusula positiva. La cláusula C es demostrable por resolución positiva a partir del conjunto de cláusulas S si existe una demostración por resolución positiva de C a partir de S. Se representa por S ResPos C . Prop.: Sea S un conjunto de cláusulas. (Adecuación) Si S ResPos , entonces S es inconsistente. (Completitud) Si S es inconsistente, entonces S ResPos . 26 / 37
27. LMF Tema 5: Resolución proposicional Reﬁnamientos de resolución Resolución positivaGrafo de resolución positiva Grafo de {{p, q}, {¬p, q}, {p, ¬q}, {¬p, ¬q}} : Traza: Paso S S 0 {1, 2, 3, 4} ∅ 1 {4, 5, 6} {1, 2, 3, 4} 2 {5, 6, 7, 8} {4, 5, 6} 3 {9} {5, 6, 7, 8} 27 / 37
28. LMF Tema 5: Resolución proposicional Reﬁnamientos de resolución Resolución negativaResolución negativa Def.: Un literal negativo es la negación de un átomo. Def.: Una cláusula negativa es un conjunto de literales negativos. Def.: Una demostración por resolución negativa es una demostración por resolución en la que en cada resolvente interviene una cláusula negativa. La cláusula C es demostrable por resolución negativa a partir del conjunto de cláusulas S si existe una demostración negativa por resolución de C a partir de S. Se representa por S ResNeg C . Prop.: Sea S un conjunto de cláusulas. (Adecuación) Si S ResNeg , entonces S es inconsistente. (Completitud) Si S es inconsistente, entonces S ResNeg . 28 / 37
29. LMF Tema 5: Resolución proposicional Reﬁnamientos de resolución Resolución unitariaResolución unitaria Def.: Una cláusula unitaria es un conjunto formado por un único literal. Def.: Una demostración por resolución unitaria es una demostración por resolución en la que en cada resolvente interviene una cláusula unitaria. La cláusula C es demostrable por resolución unitaria a partir del conjunto de cláusulas S si existe una demostración por resolución unitaria de C a partir de S. Se representa por S ResUni C . Prop.: (Adecuación) Sea S un conjunto de cláusulas. Si S ResUni , entonces S es inconsistente. 29 / 37
30. LMF Tema 5: Resolución proposicional Reﬁnamientos de resolución Resolución unitariaResolución unitaria Existen conjuntos de cláusulas S tales que S es inconsistente y S ResUni . Dem.: S = {{p, q}, {¬p, q}, {p, ¬q}, {¬p, ¬q}} Def.: Una cláusula de Horn es un conjunto de literales con un literal positivo como máximo. Ejemplos: {p, ¬q, ¬r }, {p} y {¬p, ¬q} son cláusulas de Horn. {p, q, ¬r } y {p, r } no son cláusulas de Horn. Prop.: Si S es un conjunto inconsistente de cláusulas de Horn, entonces S ResUni . 30 / 37
31. LMF Tema 5: Resolución proposicional Reﬁnamientos de resolución Resolución por entradasResolución por entradas Def.: Una demostración por resolución por entradas a partir de S es una demostración por resolución en la que en cada resolvente interviene una cláusula de S. La cláusula C es demostrable por resolución por entradas a partir del conjunto de cláusulas S si existe una demostración por resolución por entradas de C a partir de S. Se representa por S ResEnt C . Prop.: (Adecuación) Sea S un conjunto de cláusulas. Si S ResEnt , entonces S es inconsistente. Existen conjuntos de cláusulas S tales que S es inconsistente y S ResEnt . Dem.: S = {{p, q}, {¬p, q}, {p, ¬q}, {¬p, ¬q}} Prop.: Si S es un conjunto inconsistente de cláusulas de Horn, entonces S ResEnt . 31 / 37
32. LMF Tema 5: Resolución proposicional Reﬁnamientos de resolución Resolución linealResolución lineal Sea S un conjunto de cláusulas. La sucesión (C0 , C1 , . . . , Cn ) es una resolución lineal a partir de S si se cumplen las siguientes condiciones: 1. C0 ∈ S; 2. para todo i ∈ {1, . . . , n}, existe un B ∈ S ∪ {C0 , . . . , Ci−1 } tal que Ci ∈ Res(Ci−1 , B). La cláusula C0 se llama cláusula base, las Ci se llaman cláusulas centrales y las B se llaman cláusulas laterales. La cláusula C es deducible por resolución lineal a partir de S si existe una deducción por resolución lineal a partir de S, (C0 , . . . , Cn ), tal que Cn = C . Se representa por S ResLin C . Prop.: Sea S un conjunto de cláusulas. (Adecuación) Si S ResLin , entonces S es inconsistente. (Completitud) Si S es inconsistente, entonces S ResLin . 32 / 37
33. LMF Tema 5: Resolución proposicional Reﬁnamientos de resolución Resolución linealResolución lineal Ejemplo: Resolución lineal de {{p, q}, {¬p, q}, {p, ¬q}, {¬p, ¬q}} 1 {p, q} 2 {¬p, q} 3 {p, ¬q} 4 {¬p, ¬q} 5 {q} 6 {p} 7 {¬q} 8 33 / 37
34. LMF Tema 5: Resolución proposicional Argumentación por resoluciónTema 5: Resolución proposicional 1. Lógica de cláusulas 2. Demostraciones por resolución 3. Algoritmos de resolución 4. Reﬁnamientos de resolución 5. Argumentación por resolución Formalización de argumentación por resolución Decisión de argumentación por resolución 34 / 37
35. LMF Tema 5: Resolución proposicional Argumentación por resolución Formalización de argumentación por resoluciónFormalización de argumentación por resolución Problema de los animales: Se sabe que 1. Los animales con pelo o que dan leche son mamíferos. 2. Los mamíferos que tienen pezuñas o que rumian son ungulados. 3. Los ungulados de cuello largo son jirafas. 4. Los ungulados con rayas negras son cebras. Se observa un animal que tiene pelos, pezuñas y rayas negras. Por consiguiente, se concluye que el animal es una cebra. Formalización: { tiene_pelos ∨ da_leche → es_mamífero, es_mamífero ∧ (tiene_pezuñas ∨ rumia) → es_ungulado, es_ungulado ∧ tiene_cuello_largo → es_jirafa, es_ungulado ∧ tiene_rayas_negras → es_cebra, tiene_pelos ∧ tiene_pezuñas ∧ tiene_rayas_negras } Res es_cebra 35 / 37
36. LMF Tema 5: Resolución proposicional Argumentación por resolución Decisión de argumentación por resoluciónDecisión de argumentación por resolución 1 {¬ tiene_pelos, es_mamífero} Hipótesis 2 {¬ da_leche, es_mamífero} Hipótesis 3 {¬es_mamífero, ¬tiene_pezuñas, es_ungulado} Hipótesis 4 {¬es_mamífero, ¬rumia, es_ungulado} Hipótesis 5 {¬es_ungulado, ¬tiene_cuello_largo, es_jirafa} Hipótesis 6 {¬es_ungulado, ¬tiene_rayas_negras, es_cebra} Hipótesis 7 {tiene_pelos} Hipótesis 8 {tiene_pezuñas} Hipótesis 9 {tiene_rayas_negras} Hipótesis 10 {¬es_cebra} Hipótesis 11 {es_mamífero} Resolvente de 1y7 12 {¬tiene_pezuñas, es_ungulado} Resolvente de 11 y 3 13 {es_ungulado} Resolvente de 12 y 8 14 {¬tiene_rayas_negras, es_cebra} Resolvente de 13 y 6 15 {es_cebra} Resolvente de 14 y 9 16 Resolvente de 15 36 / 37 y 10
37. LMF Tema 5: Resolución proposicional BibliografíaBibliografía 1. M. Ben–Ari, Mathematical logic for computer science (2nd ed.). (Springer, 2001). Cap. 4: Propositional calculus: resolution and BDDs. 2. C.–L. Chang y R.C.–T. Lee Symbolic Logic and Mechanical Theorem Proving (Academic Press, 1973). Cap. 5.2: The resolution principle for the proposicional logic. 3. N.J. Nilsson Inteligencia artiﬁcial (Una nueva síntesis) (McGraw–Hill, 2001). Cap. 14: La resolución en el cálculo proposicional. 4. E. Paniagua, J.L. Sánchez y F. Martín Lógica computacional (Thomson, 2003). Cap. 5.7: El principio de resolución en lógica proposicional. 5. U. Schöning Logic for Computer Scientists (Birkäuser, 1989). Cap. 1.5: Resolution. 37 / 37
I1M2010-T20: El tipo abstracto de los montículos en Haskell

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 
 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 
 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 
 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 
 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 
 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 
 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 
 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 
 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 
 resolución 
 Resolución 
 resolución 
 resolución