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

Passo 1

Estamos testando a satisfatibilidade da fórmula
\neg\bigl((a \to b)\lor(b \to a)\bigr)
usando o método de Tableaux: abrimos um tableau com essa fórmula e aplicamos as regras até fechar todos os ramos ou encontrar um ramo aberto.

Passo 2

Aplicamos a regra de negação de disjunção em \neg\bigl((a \to b)\lor(b \to a)\bigr). Como \neg(P\lor Q) produz simultaneamente \neg P e \neg Q, obtemos dois ramos (que aqui podemos tratar como uma conjunção na mesma linha):
\neg(a \to b) \quad\text{e}\quad \neg(b \to a).

Passo 3

Agora aplicamos a regra de negação de implicação em cada uma:
  • De \neg(a \to b) vem a e \neg b.
  • De \neg(b \to a) vem b e \neg a.
    Assim, no ramo temos simultaneamente
a,\quad \neg b,\quad b,\quad \neg a.

Passo 4

Observamos que o ramo contém a e \neg a (contradição) e também b e \neg b. Portanto esse ramo fecha. Como esse era o único ramo, o tableau fecha por completo.

Resposta

A fórmula não é satisfazível (insatisfazível).

Exercícios relacionados