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?

  • $\begingroup$ If you use valid transformations to show that this expression results in "True", then yes, that shows this is a tautology and thus true for every possible value of $P$, $Q$, and $R$. $\endgroup$
    – Jared
    Commented Nov 19, 2014 at 6:04
  • $\begingroup$ @Jared thanks for your help :) So, basically, using resolution, I have to obtain the empty clause or a tautology to proof the implication, right? $\endgroup$
    – tigerjack
    Commented Nov 19, 2014 at 6:09
  • $\begingroup$ I hadn't heard of resolution refutation before this question. But it sounds to me like it's inferring something from axioms (does that sound correct?). If there is a single counter example, then the inference is incorrect (even though it may be true sometimes). $\endgroup$
    – Jared
    Commented Nov 19, 2014 at 6:12
  • $\begingroup$ yes, it is something like that. It tries to demonstrate that $\alpha \vDash \beta$ proofing that $\alpha \land \neg \beta$ is unsatisfiable, where $\alpha$ is a conjunction of clauses $\endgroup$
    – tigerjack
    Commented Nov 19, 2014 at 6:32

1 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 :


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.

  • $\begingroup$ thanks for your reply :) Well, I followed a different approach to convert the sentence into CNF and I ended up with 3 different tautologies. So, as you can argue, I can't apply resolution at all, because I only have something like $True \land $True \land $true$. So, I was asking if this can be considered as a proof for resolution (or maybe only the proof of the inference). $\endgroup$
    – tigerjack
    Commented Nov 19, 2014 at 10:07

You must log in to answer this question.

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