Lógica Proposicional

Tableaux semânticos

Sistema de Tableaux Semânticos

Alfabeto da Lógica Proposicional Conjunto de fórmulas da Lógica

Proposicional Conjunto de regras de dedução (ou

regras de inferência)

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

Características do Método de Tableau 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) Cada interpretação representa um

mundo possível 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 Tableau Semântico (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!!

Construção de um Tableau

Tableau 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 Tableau mais curto

Tableau 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 tableau Advindas do sistema de tableau

analítico “First Order Logic”, R. Smullyan

(1970) Adiar a bifurcação Aplicar primeiro as regras que não

bifurquem Árvore menor => menos

interpretações a serem analisadas

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

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

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

Se Tree é um tableau 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 Tableau Semântico

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

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

Exemplo de Construção de um Tableau 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 Tableau 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 Tableau 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=(P^Q^((P^R)P1)^(Q1R)^(QQ1)) P1

Mostrando que H é absurdo (P^Q^((P^R)P1)^(Q1R)^(QQ1))

P1) 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

Vimos na parte de semântica (Validade e factibilidade)

H é válida H é contraditória

Em tableaux semânticos Gerar um tableau fechado para

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

Exemplo de conjunto insatisfatível Olhando o tableau de {AvB,

(BvC), CD, (AvD)}, quais outros conjuntos de fórmulas são insatisfatíveis?

{AvB, (BvC), CD} {AvB, (BvC), (AvD)} {AvB, CD, (AvD)} {(BvC), CD, (AvD)}

Tableaux Completamente Abertos

Como provar que H é tautologia? 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ícios de Formalização

A proposta de auxílio está no correio. Se os árbitros a receberem até sexta-feira, eles a analisarão. Portanto, eles a analisarão porque se a proposta estiver no correio, eles a receberão até sexta-feira. (C, S, A)

Solução A proposta de auxílio está no correio. Se

os árbitros a receberem até sexta-feira, eles a analisarão. Portanto, eles a analisarão porque se a proposta estiver no correio, eles a receberão até sexta-feira.

C: A proposta de auxílio está no correio.S: Os árbitros recebem a proposta até Sexta-feira.A: Os árbitros analisarão a proposta.

{C, SA, CS} |-- A

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.