# 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. –  Yuval Filmus Jan 22 '13 at 18:09
I was able to remove some jargon, but was are "KB" and "KRR"? –  Raphael Jan 22 '13 at 21:05
@Raphael probably Knowledge Base (set of true sentences) and Knowledge Representation and Reasoning. –  Pål GD Jan 22 '13 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.