# Is resolution complete or only refutation-complete?

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?

• Have you read the fine print on the slide? If KB entails $f$, then you can refute KB$\land\lnot f$ using resolution. Jan 22, 2013 at 18:09
• I was able to remove some jargon, but was are "KB" and "KRR"?
– Raphael
Jan 22, 2013 at 21:05
• @Raphael probably Knowledge Base (set of true sentences) and Knowledge Representation and Reasoning. Jan 22, 2013 at 21:23

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.
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$).