Conversion to CNF - eliminate implications

Question

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.

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.