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
H
G
R2=HvG
R3=HG
H
H
R4=HG
R5=H
H
H^G H^G
R7=(HvG)
H
G
G
G
R6=(H^G)
H G
R8=(HG) R9=(HG)
H
G
H^G H^G
Regras para quantificadores
R10=(x)H
(x)H
R11= (x)H
(x)H
R12=(x)H
H(t)
R13= (x)H
H(t)
onde t é novo,
que não apareceu
na prova ainda
onde t é qualquer
R10 e 12 devem ter preferência!
Por quê???
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
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)
3. PQ
4. PQ
5. P
6. P
7. P
Q
fechado
 8.
P^Q P^Q
 9.
P
P
 10.
Q
Q
fechado fechado

R5,
R1,
R1,
R1,
R5,
1.
2.
2.
2.
5.
R3, 3.
R9, 4.
R1, 8.
R1, 8.







1. ((PQ)vP))
2. (PQ)
3. P
4. P
5. P^Q
6. P
7. Q
aberto
P^Q
P
Q
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=(P^Q^((P^R)P1)^(Q1R)^(QQ1))
P1
Mostrando que H é absurdo
(P^Q^((P^R)P1)^(Q1R)^(QQ1))
P1) gera um tableau fechado?
Exercícios de Formalização

A proposta de auxílio está no correio.
Se os árbitros a receberem até sextafeira, eles a analisarão. Portanto, eles a
analisarão porque se a proposta estiver
no correio, eles a receberão até sextafeira. (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, SA, CS} |-- 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 sextafeira, então depois de amanhã será
sábado. Conseqüentemente, se hoje for
quinta-feira, então depois de amanhã
será sábado.
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)
9. Bom(a)
fechado
Alegria
fechado
R3,3
R13,8, t=a
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))
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)
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 
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)
Fechado
Mortal(Sócrates)
Fechado
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
9. Bom(a1)
fechado
10. Bom(a2)
.... E nunca fazer x=a
R3,3
R13,8, t=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!!