Verifique se as seguintes fórmulas são satisfazíveis, através de Tableaux.
Passo 1
O enunciado pede para verificar, via Tableaux em lógica proposicional, se a fórmula
é satisfazível. Vamos usar as regras α (para conjunções e negações de implicação) e β (para disjunções).
Passo 2
Começamos com a árvore que tem, como única fórmula na raiz,
Passo 3
Aplicamos a regra α à conjunção e à negação de implicação simultaneamente:
– A conjunção gera
e
no mesmo ramo.
– A negação de implicação gera
e
.
Logo, no ramo fica
– A conjunção
– A negação de implicação
Logo, no ramo fica
Passo 4
Agora aplicamos a regra β à disjunção
, criando dois ramos:
Ramo 1: adiciona a
.
Ramo 2: adiciona a
.
Ramo 1: adiciona
Ramo 2: adiciona
Passo 5
Examinamos os ramos:
– Ramo 1 contém e
→ contradição → ramo fechado.
– Ramo 2 contém e
→ contradição → ramo fechado.
Como todos os ramos fecham, não existe atribuição de verdade que satisfaça a fórmula.
– Ramo 1 contém
– Ramo 2 contém
Como todos os ramos fecham, não existe atribuição de verdade que satisfaça a fórmula.
Resposta
A fórmula é insatisfazível (não satisfazível).