Tableaux Semantico

2.3 Tableaux Semántico

El método del Tableaux es un método utilizado para decir si una formula es satisfaccible o no, se utiliza en Cálculo Proposicional, es una herramienta muy eficiente y es utilizado también para provar teoremas generales sobre cálculo. A continuación, se presentan algunas definiciones que se utilizarán en el desarrollo del tema.

Definiciones

Átomo: Es una literal (A,P,Q,R, etc.), es el elemento mas simple, y tiene un valor de verdad.
Literal A: Es un átomo o la negación de un átomo.
Un Átomo: A
Negación de un átomo: ¬A
Un par complementario: Es una formula y su negación.
Ejemplo:
Sea la formula A, el par complementario de esta formula seria: {A,¬A}

Una formula puede ser:

Satisfacible: Se dice que una formula es satisfacible, si por lo menos una vez es verdadera.
No Satisfacible o Contradictoria: Una formula es no satisfacible, si todos los valores son falsos.
Valida (Tautologia): Se da cuando los valores de una formula son verdaderos.
No Valida o Falseable: Se da cuando alguno de los valores es falso.

Para desarrollar el Tableaux de una formula y determinar si esta es satisfacible o no, se utilizaran las siguientes tablas:

Pasos Básicos

• Se niega la formula original.
• Se desarrollan primero las reglas α .
• Una vez terminado el paso anterior, se desarrollan las reglas β .
• Si resulta un Tableaux cerrado, es decir, que en las hojas del tableaux quede un par complementario de literales, significa que la formula antes de negarse es una tautología.

Ejemplo:
Attach:tableaux_fig1.jpg Δ

Ejemplos de Desarrollo del Tableaux

Formula: (¬b → ¬a) → (a → b)

Attach:tableaux_fig2.jpg Δ
Se comprueba que (¬b → ¬a) → (a → b) es una TAUTOLOGIA
Formula: (a → (b → a))

Attach:tableaux_fig3.jpg Δ
Se comprueba que (a → (b → a)) es una TAUTOLOGIA
Formula: ((p → ¬q)^(qv¬t)^p)→ ¬t

Attach:tableaux_fig4.jpg Δ
Se comprueba que ((p → ¬q)^(qv¬t)^p)→ ¬t es una TAUTOLOGIA