# Why was the resolution method so important to AI/theorem proving?

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?

• Not quite. You might give it an interesting problem like the Goldbach Conjecture, but how then do you know beforehand if it is decidable, it could be it is undecidable and you're back to square 1. Aug 15, 2017 at 15:51
• I guess you inadvertently dropped the negation in $\Sigma, \neg \phi \vdash \bot$, but you are correct that that's what resolution-completeness of refutation means. Aug 15, 2017 at 21:37

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.
• Clausal form means CNF? I looked up Herbrand's theorem on wikipedia and I'm not exactly sure what it's saying. $(\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n}) \rightarrow \exists t_{ij} F(t_{{11}},\ldots ,t_{{1n}})\vee \ldots \vee F(t_{{k1}},\ldots ,t_{{kn}})$. Isn't that just trivial? Not even sure why we need the conjunction... just find the $n$ terms which make the formula true. Aug 15, 2017 at 23:12
• Clausal form means that the formula is in prenex form, that the matrix is in CNF and that all variables are universally quantified. As for the second question, if you find terms that make $F$ true, you proved satisfiability, not validity. The form of the theorem on the Wikipedia is the dual form of the one I mentioned. Aug 16, 2017 at 1:02