7
$\begingroup$

Going through some knowledge representation tutorials on resolution at the moment, and I came across slide 05.KR, no77.

There it is mentioned that "the procedure is also complete".

I think this completeness can not mean that if a sentence is entailed by KB, then it will be derived by resolution. For example, resolution can not derive $(q \lor \neg q)$ from a KB with single clause $\neg p$. (Example from KRR, Brachman and Levesque, page 53).

Could anyone help me figure out what is meant in this slide? Is the completeness of slide refer to being refutaton-complete and not a complete proof procedure?

Improve this question
$\endgroup$
  • 1
    $\begingroup$ Have you read the fine print on the slide? If KB entails $f$, then you can refute KB$\land\lnot f$ using resolution. $\endgroup$ – Yuval Filmus Jan 22 '13 at 18:09
  • $\begingroup$ I was able to remove some jargon, but was are "KB" and "KRR"? $\endgroup$ – Raphael♦ Jan 22 '13 at 21:05
  • 2
    $\begingroup$ @Raphael probably Knowledge Base (set of true sentences) and Knowledge Representation and Reasoning. $\endgroup$ – Pål GD Jan 22 '13 at 21:23
11
$\begingroup$

Resolution is complete as a refutation system. That is, if $S$ is a contradictory set of clauses, then resolution can refute $S$, i.e. $S \vdash \bot$.

This is sufficient since $T \vdash A$ is equivalent to $T \cup \{\lnot A\} \vdash \bot$. So if we want to see a formula $A$ is derivable from $T$, we only need to check if there is a refutation proof for $T \cup \{\lnot A\}$ which can be checked using resolution.

Improve this answer
$\endgroup$
6
$\begingroup$

Resolution is only refutationally complete, as you mentioned. This is intended and very useful, because it drastically reduces the search space. Instead of having to eventually derive every possible consequence (to find a proof of some conjecture), resolution is only trying to derive the empty clause.

Improve this answer
$\endgroup$
1
$\begingroup$

It is also implicationally complete in the following sense:

If a set of clauses $F$ implies a non tautological clause $C$, then it is always possible to derive a single clause $C'$ that subsumes $C$ (i.e. $C' \subseteq C$).

Source:
Christian G. Fermüller, Implicational Completeness of Signed Resolution, 2002

Note that the original result is refered to:
R.C.T. Lee. A completeness theorem and a computer program for nding theorems derivable from given axioms . Ph.D. Thesis, University of California, Berkely, 1967.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.