31 - Tableaux semânticos (2)

Esta é uma pré-visualização de arquivo. Entre para ver o arquivo original

*
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=HG
		 H	
 G		 H G H G 
R4=HG		R5=H 		R6=(H^G)
					H
H^G H^G				 H G	
R7=(HvG) 	R8=(HG) R9=(HG)
		H			H
		G		 G	 H^G H^G			
*
Tipos de regras - tipo α
Regras do tipo α não bifurcam
H^G, ¬(H v G), ¬(HG)
Se α=H^G, α1=H e α2=G então
 α .
α1
α2
*
Tipos de regras - tipo β
Regras do tipo β bifurcam
HvG, ¬(H ^ G), HG, HG, ¬(HG)
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 
{(AB)(AvB), (CA)}
Tree1:
1. AB
2. (AvB)
3. (CA)
*
Exemplo de Construção de um Tableaux Semântico (cont.) 
{(AB)(AvB), (CA)}
Tree2 (=R7 aplicada a Tree1):
1. AB
2. (AvB)
3. (CA)
4. A 		R7, 2.
5. B		R7, 2.
*
Exemplo de Construção de um Tableaux Semântico (cont.) 
{(AB),(AvB), (CA)}
Tree3 (=R3 aplicada a Tree2):
1. AB
2. (AvB)
3. (CA)
4. A 		R7, 2.
5. B		R7, 2.
6. A	 B	R3, 1.
*
Exemplo de Construção de um Tableaux Semântico (cont.) 
{(AB),(AvB), (CA)}
Tree4 
R8 aplicada a Tree3
O ramo da esquerda contém B e B
Como essa informação pode ser útil?
1. AB
2. (AvB)
3. (CA)
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=((PQ)^¬(PQ)^(P))??
Gerar um tableau fechado para H:
(((PQ)^¬(PQ)^(P)))
*
1. (((PQ)^¬(PQ)^(P)))
2. (PQ)^¬(PQ)^(P)			R5, 1.
3. PQ						R1, 2.
4. ¬(PQ)					R1, 2.
5. P						R1, 2.
6. P						R5, 5.
7. P	Q					R3, 3.
fechado
8.	 P^Q P^Q				R9, 4.
9. 	 P		 P				R1, 8.
10.	 Q		 Q				R1, 8.
		fechado fechado
*
1. ((PQ)vP))
2. (PQ)
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 b={H1,H2,...Hn}, 
então H é conseqüência lógica em tableaux semânticos de b 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 b={H1,H2,...Hn} em tableaux semânticos, diz-se que:
b├ 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)^(TA)^(IT)) P 
Mostrando que H é absurdo
 H=(D^I^((D^A)P)^(TA)^(IT)) H gera um tableau fechado?
*
Conjunto insatisfatível
Como provar que um conjunto de fórmulas é insatisfatível?
Por exemplo:
b={AvB, (BvC), CD, (AvD)}
*
Conjunto insatisfatível (cont.)
b é insatisfatível sse não existe I tal que
I[AvB]=I[(BvC)]=I[CD]=I[(AvD)]=T
I,I[(AvB)^(BvC)^(CD)^(AvD)]=F
I,I[((AvB)^(BvC)^(CD)^(AvD))]=T
Portanto para provar que b é insatisfatível 
Provar que ((AvB)^(BvC)^(CD)^(AvD)) é tautologia
*
Conjunto insatisfatível (cont.)
b ={AvB, (BvC), CD, (AvD)} é insatisfatível?
Provar que ((AvB)^(BvC)^(CD)^(AvD)) é tautologia
Em tableaux semânticos 
Gerar um tableau fechado para (((AvB)^(BvC)^(CD)^(AvD)))
*
Tableaux Completamente Abertos
E se eu construir um tableau direto a partir de H (e não de H)?
Ex: H=(AvA)^(AB)
Construir os tableaux de H e de H
O que um tableau completamente aberto nos diz??
*
Tableaux Completamente Abertos (cont.)
Nada!!
Ex: G=(AvA)^(BB)
Construir os tableaux de G e de G
Conclusões? 
*
Conclusões
Dada uma fórmula da lógica proposicional H
H é tautologia D Tableau associado a H é fechado
H é contraditória (insatisfatível) DH é tautologia D Tableau associado a H é fechado
H é refutável D 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.