Lógicas Clássicas
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).