Proving consequence by resolution refutation

Question

I'm having trouble figuring out my error in this exercise: the task is to prove by resolution refutation that $ p \rightarrow (q \land r)$ is a consequence of the set $\{ p \rightarrow r, (p \land r) \rightarrow q \}$.

So, I attempted this by trying to prove that

$\{ p \rightarrow r, (p \land r) \rightarrow q, \lnot(p \rightarrow (q \land r)) \}$

is unsatisfiable. The problem I'm encountering is after converting the set to CNF and trying to do the resolution. I checked the solution using Wolfram Alpha just to be sure, and it does resolve to the empty clause; but I can't see how. Here's the CNF that I got (also checked in Wolfram - all correct, it seems) that won't seem to resolve on paper:

$\{ \{ \lnot p, r \}, \{ \lnot p, q, \lnot r \}, \{ p \}, \{ \lnot q, \lnot r \} \}.$

Now, if I attempt the resolution myself, I end up with some singular literal. I've tried resolving in different orders and have only received $\{ \lnot r \}$ or $\{ \lnot p \}$ as results.

What exactly am I missing?

Answer 1

1. $¬p \lor r$

2. $¬p \lor q \lor ¬r$

3. $p$

4. $¬q \lor ¬r$

5. $r$ --- from 3) and 1)

6. $q \lor ¬r$ --- from 3) and 2)

7. $\lnot r$ --- from 4) and 6)

8. $\square$ --- from 5) and 7).

---

See Resolution: the procedure is based on the resolution rule that is nothing more than Cut rule.

The proof procedure "expands" the set of clauses, applying the rule in order to add e new clause to the original set:

The resolution rule is applied to all possible pairs of clauses that contain complementary literals. After each application of the resolution rule, the resulting sentence is simplified by removing repeated literals.

The rule has the property that preserves satisfiability, i.e. the new set of clauses is satisfiable iff the original one is.

Thus, if after iterated applications of the rule the empty clause ($\square$) is produced, being it unsatisfiable (it is another way of writing $\bot$, i.e. a contradiction) this is enough to conclude that also the original set of clauses is unsatisfiable.

But the original set is composed of the set of premises and the negation of the conclusion; thus, the conclusion is implied by the set of premises [because: $\lnot (p \land \lnot q)$ is equivalent to: $p \to q$].

---

You can see :

• Melvin Fitting, First-Order Logic and Automated Theorem Proving (1990), Ch.3.3 Propositional Resolution, page 45-on, for a complete treatment of the proof system based on the resolution rule.