Download tableros semánticos
Document related concepts
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.