Verifique se as seguintes fórmulas são satisfazíveis, através de Tableaux.
\neg(a \rightarrow b) \wedge(\neg a \vee b)

Passo 1

O enunciado pede para verificar, via Tableaux em lógica proposicional, se a fórmula
\neg(a \rightarrow b)\wedge(\neg a \vee b)
é 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,
\neg(a \rightarrow b)\wedge(\neg a \vee b).

Passo 3

Aplicamos a regra α à conjunção e à negação de implicação simultaneamente:
– A conjunção \Phi\wedge\Psi gera \Phi e \Psi no mesmo ramo.
– A negação de implicação \neg(a\rightarrow b) gera a e \neg b.
Logo, no ramo fica
a,\quad \neg b,\quad (\neg a \vee b).

Passo 4

Agora aplicamos a regra β à disjunção \neg a \vee b, criando dois ramos:
Ramo 1: adiciona \neg a a \{a,\neg b\}.
Ramo 2: adiciona b a \{a,\neg b\}.

Passo 5

Examinamos os ramos:
– Ramo 1 contém a e \neg a → contradição → ramo fechado.
– Ramo 2 contém b e \neg b → contradição → ramo fechado.
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).

Exercícios relacionados