Problem Detail: 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?
Asked By : BingWen Hui
Answered By : Yuval Filmus
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.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/9095
