1. Considere o seguinte argumento em lógica proposicional:
(\neg a \wedge \neg b) \vDash \neg(a \vee b)
Verifique se este argumento é válido usando o algoritmo da CNF, mostrando todos os passos.

Passo 1

O enunciado pede para verificar a validade do argumento
(\neg a \wedge \neg b) \vDash \neg(a \vee b)
usando o algoritmo da CNF (método de refutação por resolução). Vamos transformar as premissas e a negação da conclusão em cláusulas CNF e aplicar resolução até, se possível, obter a cláusula vazia.

Passo 2

Para testar a validade, construímos a conjunção das premissas com a negação da conclusão. As premissas são \neg a e \neg b. A conclusão é \neg(a \vee b), cuja negação é
\neg\bigl(\neg(a \vee b)\bigr)\equiv a \vee b.
Então o conjunto a verificar é
\{\neg a,\;\neg b,\;a\vee b\}.

Passo 3

Convertendo cada fórmula em cláusulas CNF (já estão em forma apropriada pois são literais ou disjunção de literais):
\neg a\quad,\quad \neg b\quad,\quad a\vee b.

Passo 4

Listamos as cláusulas resultantes:
C_1=\{\neg a\},\quad C_2=\{\neg b\},\quad C_3=\{a,b\}.

Passo 5

Aplicamos resolução:
  1. Resolva C_1=\{\neg a\} com C_3=\{a,b\} sobre o literal a.
    O resolvente é
C_4=\{b\}.
  1. Resolva C_2=\{\neg b\} com C_4=\{b\} sobre o literal b.
    O resolvente é a cláusula vazia \Box.

Passo 6

Como obtivemos a cláusula vazia, o conjunto de cláusulas é insatisfatível. Logo, (\neg a\wedge\neg b)\wedge\neg\neg(a\vee b) é inconsistente, o que implica que as premissas (\neg a\wedge\neg b) de fato entailam \neg(a\vee b).

Resposta

O argumento é válido.

Exercícios relacionados