2
$\begingroup$

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?

$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$
    – Daniel Buck
    Aug 15, 2017 at 15:51
  • $\begingroup$ 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. $\endgroup$
    – Fabio Somenzi
    Aug 15, 2017 at 21:37

1 Answer 1

Reset to default
2
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$
    – samlaf
    Aug 15, 2017 at 23:12
  • $\begingroup$ 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. $\endgroup$
    – Fabio Somenzi
    Aug 16, 2017 at 1:02

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .