Verifique se as seguintes fórmulas são satisfazíveis, através de Tableaux.
Passo 1
Estamos testando a satisfatibilidade da fórmula
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
. Como
produz simultaneamente
e
, obtemos dois ramos (que aqui podemos tratar como uma conjunção na mesma linha):
Passo 3
Agora aplicamos a regra de negação de implicação em cada uma:
- De
vem e . - De
vem e .
Assim, no ramo temos simultaneamente
Passo 4
Observamos que o ramo contém
e
(contradição) e também
e
. 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).