–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.