On the web I found a solution to an exercise on resoulution. Basically, it asks to use resolution refutation to prove $$ (P \Rightarrow (Q \Rightarrow R)) \Rightarrow ((P \Rightarrow Q) \Rightarrow (P \Rightarrow R))$$

It proceed converting the sentence into CNF and on the first step the sentence above is translated into $$ \neg (\neg (P \Rightarrow (Q\Rightarrow R))) \Rightarrow ((P \Rightarrow Q) \Rightarrow (P \Rightarrow R))$$

What kind of translation is this? Is it an error? Doesn't $\alpha \Rightarrow \beta $ translates into $\neg \alpha \lor \beta $?

My first step is like $$ \neg (\neg (P \lor (\neg Q \lor R))) \lor (\neg(\neg P \lor Q) \lor (\neg P \lor R))$$ but I don't know if it is right.

  • 1
    $\begingroup$ $\alpha$ has been translated into $\neg (\neg \alpha)$ $\endgroup$
    – Henry
    Commented Nov 18, 2014 at 22:38
  • $\begingroup$ @Henry now I see, maybe it's too late here for logic reasoning :D However, is my different first step right? What about the proof? $\endgroup$
    – tigerjack
    Commented Nov 18, 2014 at 22:49
  • $\begingroup$ @Henry WolphramAlpha returns identical results for the evaluation of first expression and my first step, but different ones for the book first step $\endgroup$
    – tigerjack
    Commented Nov 19, 2014 at 6:23
  • $\begingroup$ well, look closer it seems that it fails to translate the book first step. So, I'm not the only one who haven't understand this simplification :) $\endgroup$
    – tigerjack
    Commented Nov 19, 2014 at 6:28

1 Answer 1


For a proof by refutation you need to derive the empty clause by resolution.

I use Polish/Lukasiewicz notation. So, we have

1. C CpCqr C Cpq Cpr.

We negate it yielding

2. N C CpCqr C Cpq Cpr.

Then we get rid of all the conditionals by replacing "C" with "AN", since Cxy==ANxy.

3. N AN ANpANqr AN ANpq ANpr.

Then by a De Morgan/Petrus Hispanus law NANxy==KxNy we have

4. K ANpANqr NAN ANpq ANpr.

By the same law we have

5. K ANpANqr K ANpq NANpr.

And using the same law we then have

6. K ANpANqr K ANpq KpNr.

Then discharging the conjunctions we have four assumptions:

Assumption 1 ANpANqr.
Assumption 2 ANpq.
Assumption 3 p.
Assumption 4 Nr.

And now applying resolution we will derive the empty clause which I'll denote by "0":

Res. 1, 2  5 ANpr.
Res. 3, 5  6 r.
Res. 4, 6  7 0.

Thus, N C CpCqr C Cpq Cpr is unsatisfiable, and therefore CCpCqrCCpqCpr is satisfiable.

  • $\begingroup$ lot of interesting stuffs...at least, it seems. I can't understand your notation at all :( $\endgroup$
    – tigerjack
    Commented Nov 19, 2014 at 5:45
  • $\begingroup$ @tigerjack89 Cpq in an infix notation is (p$\rightarrow$q). Apq in the same notation is (p$\lor$q). Np is $\lnot$p. Kpq is (p$\land$q). $\endgroup$ Commented Nov 19, 2014 at 6:39
  • $\begingroup$ Thus, if we start with (P⇒(Q⇒R))⇒((P⇒Q)⇒(P⇒R)), we can abuse notation a bit and write (P⇒"Cqr")⇒("Cpq"⇒"Cpr"), then CpCqr⇒CCpq Cpr and then finally C CpCqr CCpqCpr. $\endgroup$ Commented Nov 19, 2014 at 6:42

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .