19 - Tableaux semânticos

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

Clique para editar o estilo do título mestre
Clique para editar o estilo do subtítulo mestre
*
*
*
Lógica de Predicados
Tableaux semânticos
*
*
*
Sistema de Tableaux Semânticos
Alfabeto da Lógica de Predicados
Conjunto de fórmulas da Lógica de Predicados
Conjunto de regras de dedução (ou regras de inferência)
*
*
*
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			
*
*
*
Regras novas, para quantificadores
R10=(x)H		R11= (x)H
		 (x)H			(x)H
R12=(x)H 		R13= (x)H
		H(t)				H(t)
onde t é novo,			onde t é qualquer
que não apareceu
na prova ainda
R10 e 12 devem ter preferência! 
Por quê??? 
*
*
*
Porque um termo novo (R12)?
Se H=p(x) e U=o conjunto de alunos do CIn
I[p(x)]=T D xI é inteligente
Se I[(x)p(x)]=T D pela R12 I[p(t)]=T
D pItI=T 
tI TEM que ser um aluno inteligente
não pode ser qualquer aluno
*
*
*
Porque um termo qualquer (R13)?
Se I[(x)p(x)]=T D pela R13 I[p(t)]=T
D pItI=T 
tI pode ser qualquer aluno 
Todos são inteligentes
A escolha de um t é livre
*
*
*
Características do Método de Tableau Semântico
Extensão do Tableaux proposicional
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, mas não nesta forma que iremos apresentar
*
*
*
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!!
*
*
*
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 1:
Construção de um Tableau
H=(x)(y)p(x,y)  p(a,a) é tautologia?
Tableau sobre H:
0. ((x)(y)p(x,y)  p(a,a))
1. (x)(y)p(x,y) 		R8,0
2. p(a,a) 			R8,0
3. (y)p(a,y)			R13,1 com t=a 
4. p(a,a)			R13,3 com t=a
fechado
*
*
*
Exemplo 2:
Construção de um Tableau
H=(x)p(x)  (y)p(y) é tautologia?
Tableau sobre H:
0. ((x)p(x)  (y)p(y))
1. (x)p(x)	 		R8,0
2. (y)p(y)			R8,0
3. (y)p(y)			R11,2
4. p(a)				R13,3 com t=a
4. p(a)				R13,1 com t=a
fechado
*
*
*
Exemplo 3:
Construção de um Tableau
W= (x)(Bom(x)  Alegria)  (x) (Bom(x)  Alegria)
Tableau sobre W???
*
*
*
0. ((x)(Bom(x)  Alegria)  (x) (Bom(x)  Alegria))
1. (x)(Bom(x)  Alegria) 		R8,0
2. (x) (Bom(x)  Alegria)) 		R8,0
3. (x)(Bom(x)  Alegria) 		R5,1
4. (x)(Bom(x)  Alegria) 		R11,2	
5. (x)Bom(x) 				R8,4
6. Alegria 				R8,4
7. Bom(a)					R13, t=a
8. (x)Bom(x) 	 Alegria 		R3,3
9. Bom(a)	 fechado		R13,8, t=a	
fechado
*
*
*
Exercícios
J=((x)p(x)^(x)q(x))  (x)(p(x)^q(x)) 
P=(x)(p(x)^q(x))   (x)p(x)^ (x)q(x))
Q=(x)(p(x)  (y)(p(y)) 
E outros do livro!
*
*
*
Exemplo de prova 
M=(x)(y)p(x,y)  p(a,a)
0. ((x)(y)p(x,y)  p(a,a))
1. (x)(y)p(x,y) 	R8,0
2. p(a,a)) 		R8,0
3. (y)p(t1,y) 		R12,1, t1 novo, t1=a
4. p(t1,t2)		R12,1, t2 novo, t2=a e t1
Fechado???
Se R12 fosse usada com t1 e t2=a (errado!), o tableau seria fechado
*
*
*
Exemplo 2 de prova
H=(x)p(x)^q(x)  (x)p(x) é tautologia?
Fazer o Tableau sobre H
*
*
*
Exemplo 2 de prova (cont.)
H=(x)p(x)^q(x)  (x)p(x)
0. ((x)p(x)^q(x)  (x)p(x))
1. (x)p(x)^q(x) 	R8,0
2. (y)p(x) 		R8,0
3. p(t)^q(t)		R13,1, t qualquer
4. p(t)			R1,3 
5. q(t)			R1,3
6. p(t1) 		R12,2, t1 novo, t1=t 
Aberto - Que tristeza 
*
*
*
Exemplo 2 de prova (cont.)
H=(x)p(x)^q(x)  (x)p(x)
0. ((x)p(x)^q(x)  (x)p(x))
1. (x)p(x)^q(x) 	R8,0
2. (y)p(x) 		R8,0
3. p(t) 		R12,2, t novo
4. p(t)^q(t)		R13,1, t qualquer
4. p(t)			R1,4 
5. q(t)			R1,4
6. Fechado - Que alegria 
*
*
*
Portanto, cuidado!!
Sobre uma tautologia, é possível gerar tableaux abertos e fechados associados à sua negação!
E se uma fórmula for tautologia, é possível gerar um tableau fechado associado à sua negação?
Teorema da correção é válido para tableaux semânticos de 1ª. ordem
O teorema da completude também
*
*
*
Em FOL é mais complicado...
E se é possível gerar um tableau fechado associado à negação duma fórmula, ela é tautologia?
Correção ou completude?
E se uma fórmula não for tautologia,
é possível gerar um tableau fechado associado à sua negação?
Todos os tableaux associados à sua negação são abertos?
Se foi gerado um tableau aberto associado à negação duma fórmula, ela não é tautologia?
Se só podem ser gerados tableaux abertos associado à negação duma fórmula, ela não é tautologia?
*
*
*
Mais exercícios... Fumo!!
E1=(x)(p(x)  q(x))
E2=(x)p((x)  (x)q(x))
E1  E2?? 
G1=(x)(p(x)  q(x))
G2=(x)p((x)  (x)q(x))
G1  G2?? 
G2  G1??
*
*
*
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
Porém em Lógica de 1ª. Ordem, isto é raro...
*
*
*
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
├{H1,H2,...Hn,H}
Queremos provar, por negação ao absurdo, que b U H é insatisfatível
b U H├ Falso 
*
*
*
Exercício de Cons. Lógica
{(x)(Homem(x)  Mortal(x)), Homem(Sócrates)} ├ Mortal(Sócrates)?
Prova por tableaux de
H =(x)(Homem(x)  Mortal(x))^ Homem(Sócrates))  Mortal(Sócrates)
H= ((x)(Homem(x)  Mortal(x))^ Homem(Sócrates))  Mortal(Sócrates))
*
*
*
Exercício de Cons. Lógica (cont.)
H= ((x)(Homem(x)  Mortal(x))^ Homem(Sócrates))  Mortal(Sócrates))
Por R8, queremos um tableau fechado que começa SEMPRE com as premissas e negação dõ conseqüente
1. (x)(Homem(x)  Mortal(x))^ Homem(Sócrates)) R3,0
2. (x)(Homem(x)  Mortal(x))			 R1,1
3. Homem(Sócrates)					 R1,1
4. Mortal(Sócrates) 					 R3,0
Portanto se eu gerar o conseqüente (Mortal(Sócrates)) diretamente, eu já tenho uma contradição!
Podem (e devem) usadas outras contradições
*
*
*
Exercício de Cons. Lógica (cont.)
1. (x)(Homem(x)  Mortal(x))^ Homem(Sócrates)) 
2. (x)(Homem(x)  Mortal(x))
3. Homem(Sócrates)
4. Mortal(Sócrates)
5. Homem(Sócrates)  Mortal(Sócrates)
6. Homem(Sócrates)	Mortal(Sócrates)
Fechado				Fechado
*
*
*
Conclusões
Dada uma fórmula da lógica proposicional H
H é tautologia D EXISTE um Tableau associado a H que é fechado
H é contraditória (insatisfatível) DH é tautologia D EXISTE um Tableau associado a H que é fechado
H é refutável D TODO Tableau associado a H é aberto (não necessariamente aberto completamente)
Clique para editar o estilo do título mestre
Clique para editar o estilo do subtítulo mestre
*
*
*
E para a implementação??
*
*
*
Tem um probleminha...
0. ((x)(Bom(x)  Alegria)  (x) (Bom(x)  Alegria))
1. (x)(Bom(x)  Alegria) 		R8,0
2. (x) (Bom(x)  Alegria)) 		R8,0
3. (x)(Bom(x)  Alegria) 		R5,1
4. (x)(Bom(x)  Alegria) 		R11,2	
5. (x)Bom(x) 				R8,4
6. Alegria 				R8,4
7. Bom(a)				R13, t=a
8. (x)Bom(x) 	 Alegria 	R3,3
9. Bom(a1)	 	fechado		R13,8, t=a	
10. Bom(a2)
.... E nunca fazer x=a
*
*
*
Solução
Tableaux semânticos podem ser usados, mas 
Podem não ser decidíveis (por quê?)
ocupam muita memória, para gerar as instanciações possíveis
Aguardem os próximos capítulos...
Unificação!!