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=HG H

G H G H G

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

H^G H^G H GR7=(HvG) R8=(HG) R9=(HG)

H HG G H^G H^G

Regras novas, para quantificadores

R10=(x)H R11= (x)H (x)H (x)H

R12=(x)H R13= (x)HH(t) H(t)

onde t é novo, onde t é qualquerque não apareceuna 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 xI é inteligente Se I[(x)p(x)]=T pela R12 I[p(t)]=T 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 pela R13 I[p(t)]=T 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

={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 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 ={H1,H2,...Hn} em tableaux semânticos, diz-se que: ├ H ou {H1,H2,...Hn}├ H ├{H1,H2,...Hn,H}

Queremos provar, por negação ao absurdo, que U H é insatisfatível U├ 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 EXISTE um Tableau

associado a H que é fechado H é contraditória (insatisfatível) H é

tautologia EXISTE um Tableau associado a H que é fechado

H é refutável TODO Tableau associado a H é aberto (não necessariamente aberto completamente)

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!!