Is resolution complete or only refutation-complete?

Question

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?

Answer 1

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.

Answer 2

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.

Answer 3

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.