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, via método de Tableaux, se a fórmula
é satisfatível. Se for, devemos apresentar um modelo que a torne verdadeira.
Passo 2
Aplicamos a regra da conjunção na fórmula inicial, obtendo duas fórmulas a satisfazer simultaneamente:
Passo 3
Na fórmula
usamos a regra da disjunção, gerando dois ramos:
(1A)
(1B) .
(1A)
(1B)
Passo 4
Em cada um desses ramos aplicamos a disjunção da fórmula
, o que gera, a partir de cada ramo de
, dois sub-ramos com:
Assim há quatro ramos completos, que contêm respectivamente:
(1A1)
(1A2)
(1B1)
(1B2) .
(1A1)
(1A2)
(1B1)
(1B2)
Passo 5
Expandimos a conjunção
nos ramos 1A2 e 1B2, obtendo:
(1A2)
(1B2)
— em 1B2 o fato de repetir não cria conflito.
(1A2)
(1B2)
— em 1B2 o fato de
Passo 6
Agora identificamos quais ramos ficam abertos (sem contradição):
- Ramo 1A1: tem
e . Não há e juntos → aberto. - Ramo 1A2: tem
e → fechado. - Ramo 1B1: tem
e . Não há conflito → aberto. - Ramo 1B2: tem
e . Não há em positivo para contradizer → aberto.
Há pelo menos um ramo aberto, logo a fórmula é satisfatível.
Passo 7
Extraímos um modelo de qualquer ramo aberto. Por exemplo, do ramo 1A1 tomamos as atribuições
e
pode ser arbitrário (por exemplo
). Esse modelo satisfaz
porque
é verdadeiro, e
porque
é verdadeiro.
Resposta
A fórmula é satisfatível. Um modelo possível é