Proof for the claim that finding resolution derivations is not complete.

36 Views Asked by At

I am going through this text book of knowledge representation and reasoning by Ronald J.Brachman and Hector J. Levesque. On section 4.1.1 page 53 of the book about resolution derivations ; I do not understand the proof for the claim that finding resolution derivation is not complete. The proof goes as follows-

We can have S |= c without having S |- c. For example, let S consist of the single clause [¬p] and let c be [¬q, q]. Then, S clearly entails c even though it has no resolvents. In other words, as a form of reasoning, finding Resolution derivations is sound but not complete.

How does S entail c when S has a single clause [¬p]. In other words, I understand the c evaluates to to True but unsure how S evaluates to True irrespective of the Interpretation. We could have an interpretation $ I:= p $ which makes S evaluate to False , thus S does not entail c.

1

There are 1 best solutions below

0
On BEST ANSWER

First a little note: $S$ does not evaluate to either true or false, as $S$ is a set of clauses, not a clause itself.

Now, you are right that by setting $p$ to false, the clause $[ \neg p ]$ will not be satisfied, and as clause set, $S$ will therefore not be satisfied either.

However, this does not mean that $S$ does not entail $c$. For $S$ not to entail $c$ you need to find an interpretation that satisfies $S$, but not $c$. Well, that is impossible, since any interpretation will satisfy $c$.

What you showed is that there is an interpretation that satisfies $c$, but not $S$. But that is just the wrong way around. You need to see if there is an interpretation that satisfies $S$, but not $c$.... and there isn't.