Download tableros semánticos

Document related concepts

Literal (lógica matemática) wikipedia , lookup

Resolución (lógica) wikipedia , lookup

Forma normal conjuntiva wikipedia , lookup

Metalógica wikipedia , lookup

Algoritmo DPLL wikipedia , lookup

Transcript
TABLEROS SEMÁNTICOS
En la lógica proposicional se busca principalmente la forma más fácil y eficaz de realizar una tabla
de verdad para comprobar si una formula fbf (formula bien formada) es o no una Tautología,
también cuando queremos verificar si dos fórmulas son equivalentes o no lo son o cuando
queremos verificar si hay o no implicación semántica, estas dos últimas también se pueden
reducir a determinar si una fbf es tautología.
(Ejemplo de una tautología)
Dado que encontrar la tabla de verdad de una formula depende de la cantidad de letras
proposicionales y la complejidad de la formula, existe la expresión aritmética 2^n que determina la
cantidad de filas, siendo n= letras proposicionales también debe tener tantas columnas como
subfórmulas, entonces si queremos verificar si una fórmula es tautología construimos su tabla de
verdad pero podemos encontrar un caso donde la fórmula es muy compleja y extensa y de esta
manera su tabla de verdad también lo seria.
Es ahí donde entran los tableros semánticos, basados en las ideas de E. Beth [1], que define este
método como la búsqueda sistemática de todas las posibilidades que podrían hacer falsa una
formula proposicional y observar que sea lógicamente correcta, es decir, que no se presente
ninguna contradicción, entonces se tiene un contraejemplo, si no es posible encontrar un
contraejemplo entonces tenemos que la formula proposicional el valida.
LITERALES Y FORMULAS COMPLEMENTARIAS
Un literal es una variable proposicional o su negación como por ejemplo p, q, ¬p, ¬q. un conjunto
de literales es satisfacible si y solo si no posee un par complementario de literales.
Si p es un átomo, {p, ¬p} son una pareja complementaria de literales.
Si se asigna v(p)=V entonces v(¬p)=F y viceversa
Funciona igual para las formulas
Si A es una formula, {A, ¬A} es un para complementario de formular. A es el complemento de ¬A y
viceversa
Dado los literales y las formulas complementarias entraremos a mirar su aplicación en el método
de los tableros semánticos:
Sea la formula A=(p v ¬q), el conjunto de literales está dado por: {p, ¬q} y se tiene que no es un
par complementario de literales entonces se puede establecer un modelo para A donde
A: v(p)=V, v(q)=F.
La fórmula A es satisfacible.
También se tiene que una hoja que contiene l conjunto de literales será marcada con una X, y
aquella hoja que no tenga el conjunto de literales será marcad con una O. si la hoja esta marcada
con la X será insatisfacible, es decir, no tiene modelo, en caso contrario es satisfacible, es decir,
posee modelo. El árbol que tenga todas sus hojas marcadas es llamado tablero semántico.
p v ¬p
p, ¬p
X
Como existe el par complementario de literales {p, ¬p} se puede afirmar que la fórmula es
insatisfacible
Para poder aplicar el método de los tableros semánticos son necesarias unas reglas basadas en el
conectivo principal
FORMULAS:
α Alpha: son conjuntivas y se satisfacen solo si ambas subfórmulas α1 y α2 son satisfacible
β Beta: son disyuntivas y se satisfacen aun usando solo una de las dos subfórmulas β1 y β2 es
satisfacible
si la fórmula es una negación, la clasificación, toma entre considerar ambas la negación y el
conectivo principal.
CONSTRUCCIÓN DEL TABLERO SEMÁNTICO
Tenemos la formula (p v q) Ʌ (¬p Ʌ ¬q) podemos observar que el conector principal es Ʌ, por lo
tanto podemos aplicar una formula α
Eliminamos del árbol el conector principal, en esta caso el Ʌ y se separan las subfórmulas con
coma (,).
(p v q) Ʌ (¬p Ʌ ¬q)
p v q, ¬p Ʌ ¬q
p, q, ¬p, ¬q
Podemos ver que tenemos un par complementario de literales por lo tanto la fórmula es
insatisfacible
Ahora por árbol semántico
Se elige una formula α se aplica y se genera una nueva subexpresión quedando el árbol:
p v q, ¬p, ¬q finalmente se aplica una formula β teniendo en cuenta que solo queda una
disyunción, se generan dos subexpresiones quedando el árbol con dos hojas
(p v q) Ʌ (¬p Ʌ ¬q)
p v q, ¬p Ʌ ¬q
p v q, ¬p, ¬q
p, ¬p, ¬q
X
p, ¬p, ¬q
X
Podemos observar que las dos hojas que posee el árbol cierran con X por lo tanto podemos
afirmar que la fórmula es insatisfacible por lo tanto no posee un modelo.
Referencias
[1] E. Beth. Métodos formales e introducción a la lógica simbólica y para el estudio de la eficacia
de las operaciones en la aritmética y la lógica. Reidel: Dordrecht, 1962.
[2] Manuel Sierra A. (Marzo de 2006). Caracterización deductiva de los árboles de forzamiento
semántico. Ingeniería y computación, 2 (3), 73-102.
[3] Sergio Augusto Cardona. (2011). Unidad 2: lógica proposicional: tableros semánticos.
[Diapositiva]. 12 diapositivas.
[4] Édgar J. Andrade, Pablo Cubides, Carlos M. Márquez, Esther J. Vargas, Diego Cancino. (2008).
Lógica y pensamiento formal. Colombia. Editorial Universidad del Rosario.