Tableaux

1.4. Sistemas deductivos
￿ ￿ ￿ ￿ ￿ ￿ ￿ ￿ ￿ ￿￿ ￿￿ ￿￿ ￿￿

57 {¬p, q} {¬p, r} {¬s} {¬t} {¬q, s,t} {¬s, q} {¬t, q} {p} {q} {r} {s,t} {t} {}

(8, 1) (8, 2) (9, 5) (11, 3) (12, 4)

Figura 1.20: Una derivación de la cláusula vacía Definición 1.67 (Cláusulas de Horn) Una cláusula de Horn es una cláusula con, a lo sumo, un literal positivo. Ejemplo de cláusulas de Horn son: 1. {¬p, ¬q, ¬r, s} 2.{¬p, ¬q} 3. {s} A las del primer tipo se le conoce como reglas y a las del último como hechos. Las del segundo tipo son equivalentes a un condicional como (p ∧ q) → ⊥. Analizaremos más en detalle las cláusulas de Horn cuando se aborde la resolución en Lógica de Primer Orden. Baste en este momento saber que resultan especialmente útiles no sólo porque facilitan una representación legible e intuitiva deciertos sistemas sino porque la resolución con cláusulas de Horn facilita la labor computacional.

1.4.3 Tablas semánticas
Las tablas semánticas también se denominan tablas analíticas y más comúnmente tableaux (tableau, en singular). Introducción Estrategia deductiva por refutación Las tablas semánticas proporcionan un medio sintáctico de investigar la satisfacibilidad de un conjunto. Todo loque se mencionó en (1.4.2) sobre la relación entre consecuencia y satisfacibilidad es aplicable en este punto.

58

Capítulo 1. LÓGICA DE PROPOSICIONES

Así, si desea comprobar que una fórmula es consecuencia de otras, niéguela e incorporéla a esas otras. Si resulta insatisfacible este nuevo conjunto, efectivamente existía aquella relación de consecuencia. Constatación sintáctica de lainsatisfacibilidad De nuevo, si el conjunto de partida Φ ∪ {¬ψ} era insatisfacible, en algún momento del cálculo se evidencia claramente. Intuitivamente, las fórmulas del conjunto inicial se estructuran como árbol. En particular como un árbol muy lineal, con una sola rama. Existen dos tipos de reglas de inferencia y ambas añaden nodos al árbol: una, linealmente, y otra produciendo una bifurcaciónbinaria. La satisfacibilidad de un árbol se puede comprobar en cualquier momento, considerando la satisfacibilidad de cada rama. Existen indicadores sintácticos que lo explicitan. De nuevo, la clave de estas operaciones consiste en la preservación de la satisfacibilidad. Cada aplicación de una regla amplía el árbol sin modificar la satisfacibilidad. Si el árbol original (las fórmulas de partida) eransatisfacibles así resultará el árbol ampliado en todo momento. Y si eran insatisfacibles, se llegará a constatar sintácticamente en algún momento. Notación uniforme Considere la fórmula (p ∧ ¬q). Una interpretación la satisface si y sólo si satisface a sus componentes conjuntivos. Es decir, (p ∧ ¬q) es satisfacible si y sólo si {p, ¬q} es satisfacible La fórmula propuesta era evidentementeconjuntiva. Otra fórmula como ¬(¬p ∨ q) se puede fácilmente reescribir de forma equivalente como una fórmula conjuntiva. En particular como (¬¬p ∧ ¬q). Y se satisfaría, de nuevo, si y sólo si se satisfacen simultáneamente sus componentes. Dualmente, una fórmula disyuntiva como (p ∨ ¬q) se satisface si y sólo si se satisface alguna de sus dos fórmulas inmediatas. Otras fórmulas, no explícitamentedisyuntivas como (p → ¬q) también se puede reescribir equivalentemente como (¬p ∨ ¬q). Vamos a fijar el desarrollo que se persigue con esta introducción. Observe la tabla en (fig. 1.21). Cada fórmula α de la izquierda es equivalente a la conjunción de sus componentes α1 y α2 . Y cada fórmula β, a la disyunción de sus componentes β1 , β2 . Tanto en un caso como en otro, las componentes son subfórmulas de lafórmula principal. Y a partir sólo de ellas y de sus negaciones se construye una conjunción o una disyunción equivalente a la fórmula dada. α X ∧Y ¬(X ∨Y ) ¬(X → Y ) ¬(X ← Y ) ¬(X ↑ Y ) X ↓Y X ￿→ Y X ￿← Y α1 X ¬X X ¬X X ¬X X ¬X α2 Y ¬Y ¬Y Y Y ¬Y ¬Y Y β ¬(X ∧Y ) X ∨Y X →Y X ←Y X ↑Y ¬(X ↓ Y ) ¬(X ￿→ Y ) ¬(X ￿← Y ) β1 ¬X X ¬X X ¬X X ¬X X β2 ¬Y Y Y ¬Y ¬Y Y Y ¬Y

Figura 1.21: Notación uniforme...