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 R1, …, R9 indicadas a seguir.

Regas de inferência tableaux.

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 R1, R5, R7 e R8.

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 {A1, …, An} um conjunto de fórmulas.

  • A árvore a seguir, com apenas um ramo, é um tableau associado a {A1, …, An}.
Construção tableaux1.
  • Seja T um tableau associado a {A1, …, An}. Se T* é a árvore resultante da aplicação de uma das regras R1, …, R9 à árvore T, então T* é também um tableau associado a {A1, …, An}.

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 fechado

  • Tableau semântico aberto

Tableau 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

β = {A1, ..., An},.

então H é uma consequência lógica de β, nos tableaux semânticos, se existe uma prova de

(A1 ˄ … ˄ An).

utilizando tableaux semânticos.

Referências

  • SOUZA, João Nunes de. Lógica para ciência da computação: fundamentos de linguagem, semântica e sistemas de dedução. Rio de Janeiro: Editora Campus, 2002, (cap. 8).