How is the resolution with refutation method of theorem proving different from a simple resolution rule method?

Question

I am trying to solve the question above. But arent both resolution and resolution with refutation the same?

Answer 1

I assume the difference you have in mind is this:

'resolution with refutation method': you add the negation of the conclusion to the KB, and then keep applying the resolution rule until you get an empty clause. This is what the picture shows: it negates the conclusion $\neg P_{1,2}$ and thus adds $P_{1,2}$ to the KB, and eventually it obtains an empty clause (in the far bottom right)

'simple resolution rule method': you do not add the negation of the conclusion to ht KB, but instead you keep applying the resolution rule until you get a clause that represents the conclusion.

In the picture, we note that we can get $\neg P_{1,2}$ from the clauses $\neg P_{1,2}, B_{1,1}$ and $\neg B_{1,1}$. So, you ask: why not stop right there and say that you have reached the conclusion?

Well, there are several reasons for following the first method:

First, the conclusion may not be represented by a single clause. For example, if the conclusion is $P \land Q$, then it is representation in terms of clauses is two clauses: $P$ and $Q$. So, at the very least, you'll need to verify that at some point you have obtained all of those clauses, rather than wait for a single kind of clause. This of course can still be done, but it adds a little more record-keeping to the second method.

Second, suppose the conclusion is $P \lor Q$, meaning that you need to get to $P,Q$ as a clause. Now suppose your only premise is $P$. Clearly, you cannot get to the of the goal clause using the resolution rule. However, with the refutation method, the negation of the conclusion turns to two clauses, $\neg P$ and $\neg Q$, and between $P$ and $\neg P$ you get the empty clause. Indeed, the refutation method is provably compete, but the 'simple resolution rule method' (as I understand you are trying to propose) is not: you can;t always get to the conclusion using resolution alone.