Principales aspectos de los Tableros Semánticos

El Método de Tableaux

Una lógica puede caracterizarse de distintas formas. Tradicionalmente se ha hecho mediante alguna de las tres aproximaciones siguientes:

1.    Una motivación intuitiva, quizá ligada a alguna aplicación en algún área.

2.    Una interpretación semántica.

3.    Un sistema formal de pruebas.

De entre todas las metodologías existentes en el campo de la demostración automática, hemos elegido los métodos de tableaux porque reúnen, en un único marco, las características propias de las aproximaciones orientadas al estudio de pruebas (3) y aquellas fundamentadas semánticamente (2). Además, los tableaux presentan los sistemas lógicos de una forma intuitiva (1), clara y concisa, por lo que actualmente suelen ser utilizados como el primer mecanismo deductivo que aprenden los estudiantes de lógica en la mayoría de las universidades. Por otra parte, en los últimos años se han desarrollado gran cantidad de diversos sistemas lógicos, originados por multitud de aplicaciones, para los que la metodología basada en tableaux resulta ser el mecanismo apropiado, debido a que se adaptan perfectamente a las distintas exigencias específicas. Por estos motivos, los tableaux se han extendido ampliamente y son el foco de atención de una gran cantidad de investigadores.

CARACTERÍSTICAS DEL MÉTODO DE TABLEAUX

Bajo la denominación método de tableaux se encuentran distintos sistemas deductivos

que comparten características comunes:

1. Los sistemas basados en tableaux son procedimientos formales sintácticos que generan pruebas por refutación. Esto significa que para probar que una fórmula; es válida, empezamos con alguna expresión sintáctica  que establezca que no lo es, Obviamente, esta expresión depende de la lógica sobre la que trabajemos. Hecho esto, descomponemos sintácticamente, distinguiendo casos cuando sea necesario. Esta parte del procedimiento de tableaux -etapa de expansión- puede entenderse como una generalización del proceso de transformación a forma normal disyuntiva. Una característica propia de los métodos de tableaux es el principio de subfórmula: las fórmulas introducidas en esta etapa son subfórmulas de las ya existentes’. Finalmente, estos métodos disponen de reglas para cerrar aquellos casos que impliquen condiciones sintácticas imposibles de satisfacer. Si todos los casos están cerrados, el tableaux está cerrado y tenemos una prueba de que la fórmula  no es satisfactible.

2. Desde el punto de vista semántico, un tableaux representa la búsqueda de un modelo que verifique ciertas condiciones. En este sentido, cada rama abierta de un tableaux puede considerarse como una descripción parcial de un modelo. De hecho, si estas ramas satisfacen determinadas propiedades de saturación entonces definen un modelo de la fórmula inicial. Por este motivo, los métodos de tableaux pueden usarse para generar contraejemplos.

La representación habitual de los tableaux consiste en un árbol cuyos nodos son fórmulas y que se prolonga o bifurca mediante la aplicación de las reglas anteriores. De esta forma la representación de un tableaux varía con el tiempo; de hecho deberíamos hablar de secuencias de tableaux. Desde el punto de vista semántico, debemos entender una rama como la conjunción de todas las fórmulas que contiene y a un tableaux, como la disyunción de sus ramas. Obsérvese que un nodo puede pertenecer a distintas ramas aunque sólo aparezca escrito una única vez. En este sentido, los tableaux no son redundantes pues reutilizan información en lugar de duplicaría

VENTAJAS DEL MÉTODO DE TABLEAUX

Desde el punto de vista práctico, los tableaux entrañan un indeterminismo acotado ya que satisfacen el principio de subfórmula, es decir, las fórmulas introducidas son subfórmulas de las ya existentes. De esta forma, en cada nueva expansión optarnos entre un número finito de posibilidades y la complejidad de las fórmulas no aumenta.

En el caso de la lógica de primer orden, los cuantificadores universales introducen un nuevo problema debido a que hay infinitas formas de aplicar la regla de expansión correspondiente.

Para solucionar este problema eficientemente, los tableaux hacen uso de las variables libres y de la unificación sintáctica. No obstante, como las fórmulas cuantificadas universalmente no pueden descartarse una vez usadas, el procedimiento de expansión no

acaba y el método de tableaux resulta ser un procedimiento de semidecisión (acorde con la indecidibilidad de primer orden). Todas estas razones hacen de los tableaux un mecanismo adecuado para su implementación.

Desde el punto de vista semántico, los tableaux se destacan como método pedagógico ideal para iniciarse en el mundo de la lógica. Por otra parte, la cohesión entre las reglas sintácticas del método y la semántica asociada a la lógica en cuestión, hace que los tableaux sean atractivos para una gran mayoría de los investigadores dedicados al estudio de nuevas lógicas.

IMPLEMENTACION DE MÉTODOS DE TABLEAUX

Antes de acabar el estudio de los métodos de tableaux para otras lógicas, ya se empezó a considerar su implementación. Resulta curioso comparar los objetivos iniciales de los tableaux con los de su gran competidor: la resolución. Aunque su introducción en el tiempo está próxima, Robinson en 1965 [Rob 65] diseñó la resolución corno un mecanismo de demostración automática, mientras que el objetivo inicial de los tableaux era puramente

semántico.

En 1960 Wang [Wang 60] construyó un sistema de decisión basado en tableaux para un subconjunto decidible de la lógica de primer orden, las llamadas APi-fórmulas. En r. estas fórmulas, los cuantificadores existenciales siempre preceden a los universales, por lo que la regla universal sólo necesita usar el conjunto finito de las constantes introducidas previamente por la regla existencial.

Más tarde, en [CTW 74], [Bowen 80] y [Broda 80] se introdujeron las variables libres y la unificación sintáctica de Robinson para evitar el indeterminismo incontrolado que se derivaba de la regla de expansión universal. Así, esta regla aplicada a Vxy(x) introduce

la fórmula y, donde  es una variable libre nueva que denota un elemento arbitrario, estas variables se instancian convenientemente a la hora de cerrar el tableau sin más que aplicar un mecanismo de unificación sintáctica. Esta forma de proceder áparecerá abundantemente en este trabajo.

Los sistemas de tableaux para la lógica de primer orden no necesitan ningún tipo de precomputación adicional. No obstante, el proceso de Skolemización es reconocido como una herramienta interesante que se encarga de la eliminación de los cuantificadores existenciales. De hecho, este proceso debe incorporarse implícitamente en la regla de expansión existencial cuando manejamos variables libres.

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.            

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.

[5] Pedro Jesús Martín De La Calle, Métodos de Tableaux para Lógicas, con declaratorias de términos, Madrid Mayo 2000