I have read that the resolution method was literally a "miracle" for AI. So far, from what I understand, there are 2 things differentiating from other systems of inference rules:
- Only a single inference rule is needed to prove theorems
- It is refutation complete
Which of these (or anything else that I'm missing?) makes the resolution method so important? Is it the fact that having a single inference rule makes the search procedure a lot more efficient? Or are other systems of inference not refutation complete, and hence couldn't lead to a programming language like Prolog?
Furthermore, from what I understand, being refutation-complete means that given a set of axioms $\Sigma$ and a statement $\phi$, if $\Sigma \models \phi$, then we can prove $\Sigma, \phi \vdash \bot$. This however, requires a human user to tell the system what theorem $\phi$ might be interesting. Hence, I can't see why this is so important to AI and theorem provers (they can't be left alone to guess which $\phi$ to prove since godel's theorem implies they might get stuck trying to prove something undecidable). Is this correct?
The compactness of first-order logic guarantees that validity proofs are finite. In principle, given a valid first-order sentence $\phi$, one can enumerate proofs until a proof of $\phi$ comes up. This is hardly a practical approach, though.
Herbrand's theorem says that one can focus on sets of ground clauses. The idea is that to prove the validity of $\phi$, we put $\neg \phi$ in clausal form, and we find a finite set of ground clauses that is unsatisfiable, because $\neg \phi$ is unsatisfiable if and only if such a set of clauses exists.
Finally, resolution provides a way to look for those ground clauses starting from $\neg \phi$ in clausal form. In a way, you can think of it as a clever way to look for a proof; as a way to focus on proofs that may be relevant to the goal at hand.
(Resolution relies on unification, which does not necessarily produce ground clauses. This is actually desirable: a non-ground clause can stand for many ground clauses.)
So far we have talked of first-order resolution, but propositional resolution is also fundamental for modern-day propositional decision procedures.