Is the True clause considered the proof of resolution refutation

Question

So, basically I have the sentence $$ (P \Rightarrow (Q \Rightarrow R)) \Rightarrow ((P \Rightarrow Q) \Rightarrow (P \Rightarrow R))$$ and it was asked to prove it by resolution refutation. On the last step, I found three different clauses, all true (i.e. contain stuffs like $\alpha \lor \neg \alpha \lor ...$). So, basically I obtain something like $ True \land True \land True$. It seems that WolphramAlpha confirm my results (see here). I knew that I had to derive the empty clause; so what about this case? Is it $True$ considered a proof?

Answer 1

As said in a comment, if you have applied correct transformations and showed "that this expression results in $TRUE$, that shows this is a tautology".

Resolution, as you says in your comment, is a method used to prove : $\alpha \vDash \beta$, showing the unsatisfiability of $\alpha \land \lnot \beta$.

But $\alpha \vDash \beta$ iff $\vDash \alpha \rightarrow \beta$, and $\alpha \rightarrow \beta \equiv \lnot (\alpha \land \lnot \beta)$.

Thus, showing with Resolution the unsatisfiability of $\alpha \land \lnot \beta$ is enough to prove $\vDash \alpha \rightarrow \beta$.

In order to apply Resolution to :

$(P⇒(Q⇒R))⇒((P⇒Q)⇒(P⇒R))$

we have to convert it (see your previous post) into :

$(P⇒(Q⇒R)) \land \lnot ((P⇒Q)⇒(P⇒R))$

that is :

$(\lnot P \lor \lnot Q \lor R) \land \lnot (\lnot (\lnot P \lor Q) \lor (\lnot P \lor R))$

i.e. :

$(\lnot P \lor \lnot Q \lor R) \land (\lnot P \lor Q) \land P \land \lnot R$.

This is in CNF and we have to re-write it as a set of clauses :

$\{ \lnot P \lor \lnot Q \lor R, \lnot P \lor Q, P, \lnot R \}$.

Now :

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 [trying to derive] the empty clause.