Método dos Tableaux – Wikipédia, a enciclopédia livre
Esta página ou se(c)ção precisa ser formatada para o padrão wiki. (Julho de 2011) |
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
[editar | editar código-fonte]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)
[editar | editar código-fonte]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)
[editar | editar código-fonte]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](http://upload.wikimedia.org/wikipedia/commons/4/4c/Regas_de_infer%C3%AAncia_tableaux.jpg)
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)
[editar | editar código-fonte]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](http://upload.wikimedia.org/wikipedia/commons/d/dc/Constru%C3%A7%C3%A3o_tableaux1.jpg)
- 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)
[editar | editar código-fonte]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)
[editar | editar código-fonte]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
[editar | editar código-fonte]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)
[editar | editar código-fonte]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)
[editar | editar código-fonte]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.
Referências
[editar | editar código-fonte]- 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).