Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question
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
up vote 7 down vote accepted

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.

share|cite|improve this answer

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.

share|cite|improve this answer
Thank you all for your replies – BingWen Hui Jan 25 '13 at 18:32

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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