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
