Verifique a propriedade indicada das seguintes fórmulas através de Tableaux:
(
)
, satisfatibilidade, mostrando, caso seja, o modelo para a fórmula.
(
Passo 1
O enunciado pede para verificar a satisfatibilidade da fórmula
usando Tableaux semânticos em lógica proposicional. Para isso vamos quebrar conjunções e implicações até encontrar um ramo aberto ou fechar todos os ramos.
Passo 2
Aplicamos a regra de conjunção para extrair as subfórmulas de
:
Passo 3
Transformamos as implicações em disjunções (regra β):
Agora temos três disjunções:
Passo 4
Iniciamos o tableau com
. Isso gera duas ramificações:
- Ramo A:
- Ramo B:
Passo 5
Focamos no Ramo A (onde
já vale) e desdobramos
, criando sub-ramificações:
- A1:
(redundante, pois já temos ) - A2:
Passo 6
Na sub-ramificação A2 temos
. Agora desdobramos
:
- A2a:
- A2b:
Em A2b surge e , contradição → ramo fechado.
Em A2a temos o conjuntosem contradições → ramo aberto.
Passo 7
Como há um ramo aberto,
é satisfatível. Extraímos o modelo atribuindo verdadeiros os literais do ramo aberto:
Resposta
A fórmula é satisfatível. Um modelo é