–EXEMPLO
•Inverno v Verão
•Ø Inverno v Frio
•As duas cláusulas deverão ser verdadeiras (embora pareçam independentes, são realmente conjuntas).
•Agora, observamos que apenas um entre Inverno e ØInverno será verdadeiro, em qualquer ponto. Se Inverno for verdadeiro, então Frio também deverá ser, para garantir a verdade da segunda cláusula. Se ØInverno for verdadeiro, então também Verão deverá ser, para garantir a verdade da primeira cláusula.
–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.
•
•