UNIVERSIDADE FEDERAL DE
UBERLÂNDIA
Faculdade de Ciência da Computação
Disciplina : Lógica para Ciência da Computação 2 - 20 Semestre 2005
Professora : Sandra Aparecida de Amo
Lista de Exercı́cios no 4
EXERCICIOS SOBRE MÉTODO DOS TABLEAUX
1. Fazer os seguintes exercı́cios das páginas 241, 242, 243 e 244 do Livro :
(a)
(b)
(c)
(d)
(e)
(f)
2(e), 2(g), 2(l)
3(b)
4(a), 4(c), 4(d). Corrija a fórmula em (d), colocando um ¬ na frente do último p(x).
8(e), 8(g), 8(h), 8(i)
Faça os exercicios 10(c) e 10(d).
Exercicios 12, 14, 15, 18
2. Este exercı́cio tem como objetivo mostrar que o Método dos Tableaux é correto, isto é,
se ` F então F é válida.
(a) Seja S = {F1 ,...,Fn } um conjunto de fórmulas e S’ é obtido de S aplicando-se uma
das 13 regras de inferência do método dos tableaux. Por exemplo, se S = {A ∧ B,
∀xC(x)}, então S’ pode ser {A,B,∀xC(x)}.
Mostre que se S é satisfatı́vel então S’ também é. Você tem de considerar todos os
13 casos correspondentes a cada uma das regras.
(b) Seja S um conjunto de fórmulas satisfativel e seja T um tableau para S (isto é,
uma arvore onde cada nó filho é obtido aplicando-se uma regra de inferência no nó
pai). Mostre que necessariamente existe pelo menos uma folha da árvore que é um
conjunto satisfativel de fórmulas.
(c) Mostre que se um tableau fecha para a fórmula ¬F então a fórmula ¬F deve ser
necessariamente insatisfativel (Suponha que fosse satisfativel; aplicando o item anterior, o que voce concluiria a respeito das folhas do tableau que fecha para ¬F ?)
(d) Conclua a demonstração do teorema da correção para o Método dos Tableaux.
Exercı́cios com problemas no enunciado
1
3. O exercı́cio 5 está mal formulado. Ele sugere que utilizando o método dos tableaux é
possı́vel decidir se uma dada fórmula da Lógica de Predicados é ou não válida. Isto não
é verdade : o Método dos Tableaux não decide isto, pois é provado (Teorema de Indecidibilidade de Church) que não existe um algoritmo que decida se uma fórmula da
Lógica de Predicados é válida ou não.
4.
5.
6.
7.
8.
Neste exercı́cio, você simplesmente vai tentar encontrar um tableau fechado para a negação
da fórmula. Caso encontre, você pode afirmar que a fórmula é válida. Caso não encontre
na primeira tentativa, tente novamente outras opções de aplicação das regras, CASO SO
HOUVER UM NUMERO FINITO DE POSSIBILIDADES!
Faça: 5(g), 5(l), 5(c), 5(o), 5(r)
Existe um erro no enunciado do exercı́cio 7. Você acha que é possı́vel testar todos os
tableaux para a fórmula H? (Pense na regra R13 )
Descubra o erro no enunciado do Exercicio 9. Sugestão : existe ai a mesma mal-formulação
que foi utilizada no exercı́cio 5 e que discutimos acima. O exercı́cio sugere que o Método
dos Tableaux para a Lógica de Predicados DECIDE se um conjunto de fórmulas é ou não
satisfatı́vel. Isto NÃO É VERDADE. A partir do fato de que não existe algoritmo que
decide se uma fórmula é válida ou não, conclua que não existe algoritmo que decide se
uma fórmula é satisfatı́vel ou não.
Descubra o erro no enunciado do exercı́cio 11. A única coisa que você pode fazer é tentar
encontrar um tableau que fecha. Se o encontrar, o que você pode concluir ? E se não
encontrar? Você pode concluir algo?
Descubra o erro no enunciado do exercı́cio 13. Em cada um dos itens, a única coisa que
você pode fazer é tentar encontrar um tableau que fecha. Se o encontrar, o que você pode
concluir? E se não encontrar? Você pode concluir algo?
Descubra o erro no enunciado do exercı́cio 17. A única coisa que você pode fazer é tentar
encontrar um tableau que fecha. Se o encontrar, o que você pode concluir ? E se não
encontrar? Você pode concluir algo?
EXERCICIOS EXTRAS
9. Considere a regra R12 do Método dos Tableaux :
Se ∃xA(x) então A(t), onde t é um termo novo que não aparece na fórmula ∃xA(x). Isto
é, os sı́mbolos que entram no termo t não fazem parte dos sı́mbolos que aparecem na
fórmula ∃xA(x).
(a) Mostre que esta regra não é válida.
(b) Mostre que não existe uma dedução no método dos tableaux de {∃xA(x)} ` A(t),
onde t é um termo novo, cujos sı́mbolos não aparecem na fórmula ∃xA(x).
(c) Mostre o erro na seguinte “dedução” de {∃xA(x)} ` A(t):
2
{∃xA(x),¬A(t)}
R12
{A(t),¬A(t)}
fechou
10. Considere novamente a regra R12 do Método dos Tableaux. Mostre que se ∃xA(x) é
satisfatı́vel então A(t) também é satisfatı́vel. O que você acha da recı́proca desta asserção?
11. Considere a regra R13 do Método dos Tableaux. Mostre que se ∀xA(x) é satisfatı́vel então
A(t) também é satisfatı́vel. O que você acha da recı́proca desta asserção?
12. Considere novamente as regras R10 e R11 do Método dos Tableaux. Mostre que em todas
elas :
13.
14.
15.
16.
o antecedente é satisfatı́vel se e somente se o consequente é satisfatı́vel.
Considere as regras proposicionais do método dos tableaux, isto é, as regras R1,...,R9.
Mostre que em todas elas :
o antecedente é satisfatı́vel se e somente se o consequente é satisfatı́vel.
Conclua que : na Lógica Proposicional, se um tableau para F não fecha então F não é
uma tautologia. (É possı́vel encontrar uma interpretação que satisfaz ¬F ).
Você pode concluir a mesma coisa para fórmulas da Lógica de Predicados? Por que?
Utilizando o mesmo argumento do exercı́cio anterior, conclua que : na Lógica Proposicional, se um tableau para um conjunto S de fórmulas não fecha então S é satisfatı́vel. Você
pode concluir a mesma coisa para fórmulas da Lógica de Predicados? Por que?
A partir dos exercı́cios anteriores, o que você nota de diferente entre o Método dos Tableaux para a Lógica Proposicional e o Método dos Tableaux para a Lógica de Predicados?
A partir destes exercı́cios extras você está convencido de que os enunciados dos exercı́cios
5, 7, 9, 11, 13 e 17 estão mal formulados? Explique.
3