Verifique a propriedade indicada das seguintes fórmulas através de Tableaux:
( p \vee \neg q ) \wedge((\neg p \rightarrow r) \wedge(q \rightarrow \neg r)), satisfatibilidade, mostrando, caso seja, o modelo para a fórmula.

Passo 1

O enunciado pede para verificar a satisfatibilidade da fórmula
\varphi = (p \vee \neg q)\wedge\bigl((\neg p \to r)\wedge(q \to \neg r)\bigr)
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 \varphi:
\alpha_1: p \vee \neg q, \quad \alpha_2: \neg p \to r, \quad \alpha_3: q \to \neg r.

Passo 3

Transformamos as implicações em disjunções (regra β):
\alpha_2\equiv p \vee r, \quad \alpha_3\equiv \neg q \vee \neg r.
Agora temos três disjunções:
\beta_1: p \vee \neg q, \quad \beta_2: p \vee r, \quad \beta_3: \neg q \vee \neg r.

Passo 4

Iniciamos o tableau com \beta_1. Isso gera duas ramificações:
  • Ramo A: p
  • Ramo B: \neg q

Passo 5

Focamos no Ramo A (onde p já vale) e desdobramos \beta_2\colon p \vee r, criando sub-ramificações:
  • A1: p (redundante, pois já temos p)
  • A2: r

Passo 6

Na sub-ramificação A2 temos \{p,r\}. Agora desdobramos \beta_3\colon \neg q \vee \neg r:
  • A2a: \neg q
  • A2b: \neg r Em A2b surge r e \neg r, contradição → ramo fechado.
    Em A2a temos o conjunto \{p,\,r,\,\neg q\} sem contradições → ramo aberto.

Passo 7

Como há um ramo aberto, \varphi é satisfatível. Extraímos o modelo atribuindo verdadeiros os literais do ramo aberto:
p = \text{V},\quad q = \text{F},\quad r = \text{V}.

Resposta

A fórmula é satisfatível. Um modelo é
p = \text{V},\quad q = \text{F},\quad r = \text{V}.

Exercícios relacionados