Lógicas Clássicas
Resolução
A BASE DA RESOLUÇÃO
- Assim, dessas duas cláusulas, podemos deduzir que
- Verão v Frio
- Esta é a dedução feita pelo procedimento de resolução.
- A resolução opera tirando suas cláusulas que contenham cada uma, o mesmo literal, neste exemplo Inverno.
- O literal deverá ocorrer na forma positiva numa cláusula e na forma negativa na outra.
- O resolvente é obtido combinando-se todos os literais das duas cláusulas paternas, exceto aqueles que se cancelam.
- Se a cláusula produzida for vazia, então foi encontrada uma CONTRADIÇÃO, o que valida a fórmula.