Verifique a validade das seguintes fórmulas, utilizando o método da CNF:
Passo 1
O enunciado pede para verificar a validade da fórmula
usando o método de CNF (forma normal conjuntiva) e resolução. Isso faz parte de lógica proposicional, e vamos mostrar que a negação da fórmula é insatisfatível, provando assim que a fórmula é uma tautologia.
Passo 2
Uma fórmula
é válida (tautologia) se, e somente se, a sua negação
for insatisfatível. Portanto, definimos
e vamos testar a insatisfatibilidade de
Passo 3
Simplificamos
usando equivalências lógicas:
onde
e
. Logo
Em seguida,
portanto
E finalmente
de modo que
Passo 4
Escrevemos
em CNF como um conjunto de cláusulas:
gera as cláusulas
Passo 5
Aplicamos o método de resolução:
- Resolva
e :
e resolvem sobre , produzindo
- Resolva
e :
e resolvem sobre , produzindo a cláusula vazia .
A obtenção de
mostra que
é insatisfatível.
Resposta
A fórmula
é válida (tautologia).