# Conversion to CNF - eliminate implications

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.

• $\alpha$ has been translated into $\neg (\neg \alpha)$ Commented Nov 18, 2014 at 22:38
• @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? Commented Nov 18, 2014 at 22:49
• @Henry WolphramAlpha returns identical results for the evaluation of first expression and my first step, but different ones for the book first step Commented Nov 19, 2014 at 6:23
• 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 :) Commented Nov 19, 2014 at 6:28

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.

• lot of interesting stuffs...at least, it seems. I can't understand your notation at all :( Commented Nov 19, 2014 at 5:45
• @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). Commented Nov 19, 2014 at 6:39
• 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. Commented Nov 19, 2014 at 6:42