Lógica de Predicados (tableaux)

Lógica de Predicados

Tableaux semânticos

Lógica de Predicados – Tableau semântico

Sequência de fórmulas que se apresenta sob a forma de uma árvore, construída de forma análoga aos tableaux da Lógica Proposicional

Elementos básicos 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)

Utiliza a linguagem da Lógica de Predicados Extensão do tableau da Lógica Proposicional Construção e conceitos de tableau fechado são os mesmos

apresentados na lógica proposicional

Regras

Regras novas

Método de prova

Uma prova de H usando tableaux semânticos é um tableau fechado associado a ¬H

H é um teorema do sistema de tableaux semânticos

Construção de um tableau

H=(∀x)(∀y)p(x,y) p(a,a) é tautologia? Tableau sobre ¬H:

1. ¬((∀x)(∀y)p(x,y) p(a,a))2. (∀x)(∀y)p(x,y) R8,13. ¬p(a,a) R8,14. (∀y)p(a,y) R13,2 faça t=a 5. p(a,a) R13,4 faça t=afechado

Construção de um tableau

H=(∀x)p(x) (∃y)p(y) é tautologia? Tableau sobre ¬H:

1. ¬((∀x)p(x) (∃y)p(y))2. (∀x)p(x) R8,13. ¬(∃y)p(y) R8,14. (∀y)¬p(y) R11,35. ¬p(a) R13,4 faça t=a6. p(a) R13,2 faça t=afechado

Tableau semântico

H=(∃x)(∃y)p(x,y) → p(a,a)1. ¬((∃x)(∃y)p(x,y) → p(a,a))2. (∃x)(∃y)p(x,y) R8,13. ¬p(a,a) R8,14. (∃y)p(t1,y) R12,2, x = t1, t1 é novo, t1≠a5. p(t1,t2) R12,4, y = t2, t2 é novo, t2 ≠ a, t2 ≠t1Fechado???

Se R12 fosse usada com t1 e t2=a, o tableau seria fechado, porém a regra não permite.

Tableau aberto!

Tableau semântico

H=(∀x)(p(x)∧q(x)) → (∀x)p(x)1. ¬((∀x)(p(x) ∧ q(x)) → (∀x)p(x))2. (∀x)(p(x) ∧ q(x)) R8,13. ¬(∀x)p(x) R8,14. (∃x) ¬p(x) R10,35. p(t) ∧ q(t) R13,2, t é qualquer6. p(t) R1,5 7. q(t) R1,58. ¬p(t1) R12,4, t1 é novo, t1 ≠ t Aberto.

Tableau semântico

H=(∀x)(p(x)∧q(x)) → (∀x)p(x)1. ¬((∀x)(p(x) ∧ q(x)) → (∀x)p(x))2. (∀x)(p(x) ∧ q(x)) R8,13. ¬(∀x)p(x) R8,14. (∃x) ¬p(x) R10,35. ¬p(a) R12,46. p(a) ∧ q(a) R13,2, faça t = a5. p(a) R1,6 6. q(a) R1,6Fechado.

Conclusões

Se H é tautologia, então existe tableau fechado associado a H Se H não é tautologia, então não existe tableau fechado

associado a H Se H não é tautologia, então todo tableau associado a H é aberto Se um tableau associado a H é fechado, então H é tautologia

Exercícios

W= (∀x)(B(x) → A) →(∃x) (B(x) → A) Tableau sobre ¬W???

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