- Considere o seguinte argumento em lógica proposicional:
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
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
e
. A conclusão é
, cuja negação é
Então o conjunto a verificar é
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):
Passo 4
Listamos as cláusulas resultantes:
Passo 5
Aplicamos resolução:
- Resolva
com sobre o literal .
O resolvente é
- Resolva
com sobre o literal .
O resolvente é a cláusula vazia.
Passo 6
Como obtivemos a cláusula vazia, o conjunto de cláusulas é insatisfatível. Logo,
é inconsistente, o que implica que as premissas
de fato entailam
.
Resposta
O argumento é válido.