–EXEMPLO
•"x "y (($ z (P(x,z) ^ P(y,z)) ® $ u Q(x,y,u)) =
•"x "y (Ø ($ z (P(x,z) ^ P(y,z))) v $ u Q(x,y,u)) =
•"x "y ("z (Ø P(x,z) v Ø P(y,z))) v $ u Q(x,y,u)) =
•"x "y "z$ u (Ø P(x,z) v Ø P(y,z) v Q(x,y,u))
•"x "y "z (Ø P(x,z) v Ø P(y,z) v Q(x,y,f(x,y,z)))
•Ø P(x,z) v Ø P(y,z) v Q(x,y,f(x,y,z))
•que é perfeitamente equivalente à fórmula original.
•Resolução
–Seria útil, do ponto de vista computacional, que tivéssemos um procedimento de prova que realizasse, em uma única operação, a variedade de processos envolvidos no raciocínio, com declarações da lógica dos predicados.
–Este procedimento é a RESOLUÇÃO, que ganha sua eficiência por operar em declarações que foram convertidas à forma clausal, como mostrado anteriormente.
–A Resolução produz provas por REFUTAÇÃO, ou seja, para provar uma declaração (mostar que ela é válida), a resolução tenta demonstar que a negação da declaração produz uma contradiçãp com as declarações conhecidas (não é possível de ser satisfeita).
–É 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.