9

TABLEAUX SEMÂNTICOS NA LÓGICA PROPOSICIONAL

Os tableaux semânticos e a resolução são sistemas de dedução, que também estabelecem estruturas que permitem a representação e a dedução formal de conhecimento. São mais adequados para implementações em computadores.

É uma seqüência de fórmulas construída de acordo com certas regras e geralmente apresentada sob a forma de uma árvore. Os elementos básicos que compõem esta árvore são definidos a seguir.
ELEMENTOS BÁSICOS DE UMA TABLEAU SEMÂNTICO ü O alfabeto da Lógica Proposicional ü O conjunto das fórmulas da Lógica Proposicional ü Um conjunto de regras de dedução
Observem que os elementos básicos de um tableau semântico determinam sua estrutura. 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:

A prova no tableaux semânticos é 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 esse 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. Considere o exemplo a seguir, onde se tem a construção de um tableau. Considere o conjunto de fórmulas:
{(A ∨ B), (A ∧ ¬B)}
O tableau semântico construído a partir destas fórmulas é dado por

O tableau semântico é inicializado com as fórmulas (A ∨ B) e (A ∧ ¬B) que são as fórmulas .1 e .2. Em seguida, a regra R2 é aplicada à fórmula .1, obtendo-se as fórmulas
.3. Finalmente, a regra R1 é aplicada à fórmula .2 e são obtidas as fórmulas .4 e .5.
Observe que a aplicação da regra R2 faz com que o tableau semântico se bifurque em dois ramos. O mesmo não ocorre com a aplicação de R1, cujos resultados são repetidos nos dois ramos do tableau. Este tableau também pode ser construído pela