Lógicas Clássicas
Resolução
A BASE DA RESOLUÇÃO
- É um processo interativo onde, em cada passo, duas cláusulas, denominadas cláusulas paternas, são comparadas (resolvidas), resultando em uma nova cláusula, dela inferida.
- A nova cláusula representa maneiras em que as duas cláusulas paternas interagem entre si.
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.