Lógica Proposicional

Tableaux semânticos

Características do Método de Tableaux Semântico

Baseado em árvores Ramos são decomposições de H em

subfórmulas ou seja, possibilidades de

interpretações da fórmula Cada ramo representa uma ou mais

interpretações Adequado para implementação!

Idéia Básica de Tableaux Semânticos Concebido por E. Beth (1954) e

Jaako Hintikka (1955) Interpretação – caminho da raiz da

árvore a uma folha “Semântica dos Mundos Possíveis” Buscam admissões de

interpretações

Características do Método de Tableaux(cont.)

Sistema de refutação Prova por negação ou absurdo Para provar H supõe-se

inicialmente, por absurdo, H As deduções desta fórmula levam a

um fato contraditório (ou absurdo) Então H é verdade!!

R1=H^G R2=HvG R3=HG H

G H G H G

R4=HG R5=H R6=(H^G)

HH^G H^G H G

R7=(HvG) R8=(HG) R9=(HG)

H HG G H^G

H^G

Tipos de regras - tipo α

Regras do tipo α não bifurcam H^G, ¬(H v G), ¬(HG) Se α=H^G, α1=H e α2=G então α .α1α2

Tipos de regras - tipo β

Regras do tipo β bifurcam HvG, ¬(H ^ G), HG, HG,

¬(HG) Se β=HvG, β1=H e β2=G então

β

Β1 β2

Construção de um Tableaux

Tableaux semântico para o conjunto de fórmulas {(AvB),(A^ B)}

1. AvB 2.A^ B

3. A B R2, 1. 4. A A R1, 2. 5. B B R1, 2.

Construção do mesmo Tableaux mais curto

Tableaux semântico para o conjunto de fórmulas {(AvB),(A^ B)}

1. AvB 2.A^ B 3. A R1, 2. 4. B R1, 2.

5. A B R2, 1.

Heurística para aplicação de regras para tableaux Adiar a bifurcação Aplicar primeiro as regras que não

bifurquem Árvore menor => menos

interpretações a serem analisadas

Construção de um Tableaux Semântico – Definição (recursiva)

Dado o conjunto de fórmulas {A1,A2,...,An}

A seguinte árvore, com um ramo, é um tableaux associado a {A1,A2,...,An} 1. A1 2. A2, ... n. An

Se Tree é um tableaux associado a {A1,A2,...,An}, então Tree* (Tree submetida a alguma das regras R1 a R9) também é

Exemplo de Construção de um Tableaux Semântico

{(AB)(AvB), (CA)} Tree1:

1. AB 2. (AvB) 3. (CA)

Exemplo de Construção de um Tableaux Semântico (cont.)

{(AB)(AvB), (CA)} Tree2 (=R7 aplicada a Tree1):

1. AB 2. (AvB) 3. (CA) 4. A R7, 2. 5. B R7, 2.

Exemplo de Construção de um Tableaux Semântico (cont.) {(AB),(AvB), (CA)} Tree3 (=R3 aplicada a Tree2):

1. AB 2. (AvB) 3. (CA) 4. A R7, 2. 5. B R7, 2.

6. A B R3, 1.

Exemplo de Construção de um Tableaux Semântico (cont.) {(AB),(AvB),

(CA)} Tree4

R8 aplicada a Tree3 O ramo da

esquerda contém B e B Como essa

informação pode ser útil?

1. AB 2. (AvB) 3. (CA) 4. A R7, 2. 5. B R7, 2.

6. A B R3, 1 7. C C R8, 3. 8. A A R8, 3.

Ramo aberto e fechado

Ramo fechado – contém uma fórmula B e sua negação B, ou o símbolo de verdade false

Tableau fechado – não contém ramos abertos

Prova e Teorema em Tableaux Semânticos

Uma prova de H usando tableaux semânticos é ... Um tableau fechado associado a... H! Neste caso, H é um teorema do

sistema de tableaux semânticos

Exemplo de Prova em Tableaux Semânticos

Como provar H=((PQ)^¬(PQ)^(P))??

Gerar um tableau fechado para H: (((PQ)^¬(PQ)^(P)))

1. (((PQ)^¬(PQ)^(P))) 2. (PQ)^¬(PQ)^(P) R5, 1. 3. PQ R1, 2. 4. ¬(PQ) R1, 2. 5. P R1, 2. 6. P R5, 5.

7. PQ R3, 3.fechado 8. P^Q P^Q R9, 4. 9. P P R1, 8. 10. Q Q R1, 8.

fechado fechado

1. ((PQ)vP)) 2. (PQ) 3. P

4. P^Q P^Q 5. P P 6. Q Q

aberto fechado

Conseqüência Lógica em Tableaux Semânticos Dada uma fórmula H e um conjunto de hipóteses

={H1,H2,...Hn}, então H é conseqüência lógica em

tableaux semânticos de se existe uma prova, usando tableaux semânticos de (H1^H2^...^Hn) H

Notação de Conseqüência Lógica em Tableaux Semânticos

Dada uma fórmula H, se H é conseqüência lógica de um conjunto de hipóteses ={H1,H2,...Hn} em tableaux semânticos, diz-se que: ├ H ou {H1,H2,...Hn}├ H

Exemplo de Conseqüência Lógica em Tableaux Semânticos

Guga é determinado Guga é inteligente Se Guga é determinado, ele não é um

perdedor Guga é um atleta se é amante do tênis Guga é amante do tênis se é inteligente

“Guga não é um perdedor” é conseqüência lógica das afirmações acima??

Solução

Provar H H=(D^I^((D^A)P)^(TA)^(IT)) P

Mostrando que H é absurdo H=(D^I^((D^A)P)^(TA)^(IT))

H gera um tableau fechado?

Conjunto insatisfatível

Como provar que um conjunto de fórmulas é insatisfatível?

Por exemplo: ={AvB, (BvC), CD, (AvD)}

Conjunto insatisfatível (cont.)

é insatisfatível sse não existe I tal que I[AvB]=I[(BvC)]=I[CD]=I[(AvD)]=T

I,I[(AvB)^(BvC)^(CD)^(AvD)]=F I,I[((AvB)^(BvC)^(CD)^(AvD))]=T

Portanto para provar que é insatisfatível Provar que ((AvB)^(BvC)^(CD)^(AvD)) é

tautologia

Conjunto insatisfatível (cont.) ={AvB, (BvC), CD, (AvD)} é

insatisfatível? Provar que

((AvB)^(BvC)^(CD)^(AvD)) é tautologia

Em tableaux semânticos Gerar um tableau fechado para

(((AvB)^(BvC)^(CD)^(AvD)))

Tableaux Completamente Abertos

E se eu construir um tableau direto a partir de H (e não de H)? Ex: H=(AvA)^(AB) Construir os tableaux de H e de H

O que um tableau completamente aberto nos diz??

Tableaux Completamente Abertos (cont.)

Nada!! Ex: G=(AvA)^(BB) Construir os tableaux de G e de G Conclusões?

Conclusões

Dada uma fórmula da lógica proposicional H H é tautologia Tableau associado a H é

fechado H é contraditória (insatisfatível) H é

tautologia Tableau associado a H é fechado H é refutável Tableau associado a H é

aberto (não necessariamente aberto completamente)

Exercício

Hoje é Sábado ou Domingo. Se hoje é Sábado então é um fim de semana. Se hoje é Domingo então é um fim de semana. Portanto, hoje é um fim de semana.

Exercício Se hoje é Quinta-feira, então

amanhã será sexta-feira. Se amanhã for sexta-feira, então depois de amanhã será sábado. Conseqüentemente, se hoje for quinta-feira, então depois de amanhã será sábado.