# Método dos Tableaux

Os tableaux semânticos são um sistema de dedução que também estabelece estruturas que permitem a representação e a dedução formal de conhecimento. O tableaux semântico é mais adequado para implementações em computadores. O método de tableaux semânticos foi inventado pelos estudiosos de lógica holandeses Evert Willem Beth e Jaakko Hintikka.

## Tableaux Semânticos na Lógica Proposicional

Um tableau semântico na Lógica Proposicional é uma sequência de fórmulas construída de acordo com certas regras e geralmente apresenta a forma de uma árvore. Os elementos básicos que compõem esta árvore são definidos a seguir.

### Definição (elementos básicos de um tableau semântico)

Os elementos básicos de um tableau semântico na Lógica Proposicional são definidos pela composição dos elementos:
   * O alfabeto da Lógica Proposicional;
   * O conjunto das fórmulas da Lógica Proposicional
   * Um conjunto de regras de dedução.
O tableau semântico contém apenas regras de dedução, que definem o mecanismo de inferência, permitindo a dedução de conhecimento. As regras são definidas a seguir.

### Definição (regras de inferência do tableau semântico)

Sejam A e B duas fórmulas da Lógica Proposicional. As regras de inferência do tableau semântico na Lógica Proposicional são R$_1$, …, R$_9$ indicadas a seguir.
O método de prova nos tableaux é feita utilizando o método da negação ou absurdo. Assim, para provar uma fórmula A, é considerada inicialmente a sua negação ¬A. Em seguida, o tableau semântico associado a ¬A é construído. Devido a este fato, tal sistema também é denominado como um sistema de refutação. O tableau semântico é construído a partir de ¬A utilizando as regras de dedução, cuja aplicação decompõe a fórmula ¬A em subfórmulas.
Em geral, a aplicação de uma regra a um tableau é feita considerando qualquer uma das fórmulas. Entretanto, uma boa heurística na construção do tableau é aplicar inicialmente regras que não bifurcam a árvore. Aplique preferencialmente as regras R$_1$, R$_5$, R$_7$ e R$_8$.
A construção de um tableau semântico é definida recursivamente a seguir.

### Definição (construção de um tableau)

Um tableau semântico, na Lógica Preposicional, é construído como se segue. Seja {A$_1$, …, A$_n$} um conjunto de fórmulas.
   * A árvore a seguir, com apenas um ramo, é um tableau associado a {A$_1$, …, A$_n$}.
   * Seja T um tableau associado a {A$_1$, …, A$_n$}. Se T* é a árvore resultante da aplicação de uma das regras R$_1$, …, R$_9$ à árvore T, então T* é também um tableau associado a {A$_1$, …, A$_n$}.

### Definição (ramo fechado e aberto)

Um ramo em um tableau é fechado se ele contém uma fórmula A e sua negação ¬A ou contém o símbolo de verdade false. Um ramo é aberto quando não é fechado.

### Definição (tableau fechado)

Um tableau é fechado quando todos os seus ramos são fechados. Caso contrário, ele é aberto. Exemplos:
* Tableau semântico fechado
* Tableau semântico aberto

## Consequência Lógica em Tableaux Semânticos

Os tableaux semânticos definem uma estrutura para representação e dedução de conhecimento. Utilizando as regras de inferência, são construídas árvores que determinam um mecanismo de inferência. É definido a seguir a prova de uma fórmula utilizando tableau semântico. Em seguida, a definição de consequência lógica é considerada.

### Definição (prova e teorema em tableaux semânticos)

Seja H uma fórmula. Um prova de H utilizando tableaux semânticos é um tableux fechado associado a ¬H. Neste caso, H é um teorema do sistema de tableaux semânticos.

### Definição (consequência lógica em tableaux semânticos)

Dada uma fórmula H e um conjunto de hipóteses
então H é uma consequência lógica de β, nos tableaux semânticos, se existe uma prova de
utilizando tableaux semânticos.