10. tableaux lp

Prévia do material em texto

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. 
Alírio
Highlight
Alírio
Highlight
Alírio
Highlight
Alírio
Highlight
Alírio
Highlight
Alírio
Highlight
 
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 aplicação de R1 e depois 
R2. Neste caso, o resultado é o tableau 
 
 
 
Neste último tableau, R2 é aplicada após R1. Isto significa que a bifurcação da árvore é 
postergada. Em geral, a aplicação de uma regra a um tableau é feita considerando 
qualquer uma das fórmulas presentes na árvore. Entretanto, uma boa heurística na 
construção do tableau é aplicar inicialmente regras que não bifurcam a árvore. 
 
Þ Heurística (aplicação de regras). Aplique preferencialmente as regras 
 R1, R5, R7 e R8, que não bifurcam o 
 tableau. 
 
 
Alírio
Highlight
Alírio
Highlight
Alírio
Highlight
Alírio
Highlight
Alírio
Highlight
Alírio
Highlight
 
 
 
 
Exemplo(construção de um tableau semântico). Considere o conjunto de fórmulas. 
{(A®B), Ø(A Ú B), Ø(C ® A)} 
 
Conforme a definição anterior, a árvore de apenas um ramo Tree1, é um tableau associado 
ao conjunto de fórmulas anteriores. 
 
 
 
 
O resultado da aplicação de R7 a Tree1 é dado por Tree2. 
 
 
 
Alírio
Highlight
 
O tableau Tree3, a seguir, é o resultado da aplicação de R3 a Tree2. 
 
 
 
Finalmente, após a aplicação de R8 à árvore Tree3, tem-se 
 
 
 
Obs.: o ramo à esquerda contem uma contradição (B e ØØB) 
 
 
 
RAMO FECHADO E RAMO ABERTO 
 
Definição: 
 
Þ Um ramo em um Tableau é fechado se ele contem 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. 
 
 
 
 
Alírio
Highlight
TABLEAU FECHADO 
 
Definição: 
 
Þ Um tableau é fechado quando todos os seus ramos são fechados. Caso contrário, ele 
é 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 regras de inferência, são construídas árvores que determinam um 
mecanismo de inferência. 
 
 
PROVA, TEOREMA E TABLEAUX SEMÂNTICOS 
 
Definição: 
 
Þ Seja H uma fórmula. Uma prova de H utilizando tableaux semânticos é um tableau 
fechado associado a Ø H. Neste caso, H é um teorema do sistema tableaux 
semânticos. 
 
 
Exemplos: 
 
1) H = Ø((P ® Q) Ù Ø(P « Q) Ù ØØP) 
 
 
 
Alírio
Highlight
Alírio
Highlight
Alírio Nunes
Realce
 
 
 
 
2) G = (Ø(P « Q) Ú ØØP) 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
Teorema da Completude. Seja H uma fórmula da Lógica Proposicional. Se H é uma
tautologia então existe uma prova de H no sistema Tableaux Semânticos.
O sistema de tableaux semânticos também é correto. Todo teorema é uma tautologia. Isto
significa que dada uma fórmula H, se o tableau associado a ØH é fechado, então H é uma 
tautologia. Em outras palavras, os argumentos provados utilizando tableaux semânticos são 
válidos.
CONSEQUÊNCIA LÓGICA EM TABLEAUX SEMÂNTICOS
Dada uma fórmula H e um conjunto de hipóteses b = {A1, ..., An}, então H é uma
conseqüência lógica de b , nos tableaux semânticos, se existe uma prova de
(A1 Ù ... Ù An) ® H
utilizando tableaux semânticos.
Notação. Dada uma fórmula H, se H é conseqüência lógica de um conjunto de hipóteses
b = {A1, ..., An}, nos tableaux semânticos, então este fato é indicado pela notação
b ½¾ H ou {A1, ..., An} ½¾ H
Exemplo 1. Considere o argumento
Guga é determinado
Guga é inteligente 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
Se Guga é determinado e atleta, ele não é um perdedor
Guga é um atleta se é um amante do tênis
Guga é amante do tênis se é inteligente
A afirmação “Guga não é um perdedor” é uma conseqüência lógica das premissas
acima?
Uma prova utilizando tableaux semânticos é feita para responder essa questão. 
Considere inicialmente as seguintes correspondências:
P = Guga é determinado
Q = Guga é inteligente
R = Guga é atleta
P1 = Guga é um perdedor e
Q1= Guga é amante do tênis. 
 
Traduzindo para a Lógica Proposicional temos, 
 
H = (P Ù Q Ù ((P Ù R) ® ØP1) Ù (Q1 ® R) Ù (Q ® Q1)) ® ØP1 
 
Deve-se provar então se H é ou não uma tautologia. Em outras palavras, deve-se provar se 
½¾ H. 
 
Alirio Nunes
Destacar
Þ Como o tableau é fechado, então H é uma tautologia e a conseqüência lógica 
ocorre. 
 
Exemplo 2(conjunto insatisfatível). Este exemplo demonstra, utilizando tableaux 
semânticos, que o conjunto de fórmulas a seguir é insatisfatível. 
b = { ØA Ú B, Ø(B Ú ØC), C ® D, Ø(ØA Ú D)} 
Observe que b é insatisfatível se e somente se não existe interpretação I tal que: