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?