I came across resolution inference rule stating:

$((p\lor q)\land (\lnot p\lor r))\rightarrow(q\lor r)$

I googled a lot but what I get is either the proof using truth table or using this to prove others.

Then I tried something like this:

$LHS \equiv (p\lor q)\land (\lnot p\lor r)$

$\equiv (p\land \lnot p)\lor(p\land r)\lor (q\land \lnot p)\lor (q\land r)$

$\equiv (p\land r)\lor (q\land \lnot p)\lor (q\land r)$

But I cannot move further.

I also tried to prove the whole statement to true:

$(p\lor q)\land (\lnot p\lor r) \leftrightarrow (q\lor r)$

$\equiv \lnot((p\lor q)\land (\lnot p\lor r)) \lor (q\lor r)$

$\equiv \lnot(p\lor q)\lor \lnot(\lnot p\lor r) \lor (q\lor r)$

$\equiv (\lnot p\land \lnot q)\lor (p\land \lnot r) \lor (q\lor r)$

But I am unable to solve this further to equate this to TRUE. Where I am going wrong?


3 Answers 3


Resolution is not an equivalence.

The easiest way to derive it is to use the tautological equivalence between : $A \to B$ and $\lnot A \lor B$.

Thus :


is equivalent to :

$(\lnot q \to p) \land (p \to r).$

Then, applying Hypothetical syllogism, we get :

$\lnot q \to r$

i.e. : $q \lor r$.

  • $\begingroup$ this was super easy $\endgroup$
    – Maha
    Dec 26, 2015 at 15:45
  • $\begingroup$ @Mauro ALLEGRANZA, but isn't that an equivalence in itself? $\endgroup$ Jul 18, 2017 at 14:03
  • 1
    $\begingroup$ @BeshalJaenal - the equivalence between $p \to q$ and $\lnot p \lor q$ is an equivalence indeed, but the rule of HS: "from $p \to q$ and $q \to r$, infer $p \to r$" is not. $\endgroup$ Jul 18, 2017 at 14:06
  • $\begingroup$ @MauroALLEGRANZA, How come? What's the difference? $\endgroup$ Jul 18, 2017 at 15:02

Using the equivalences $A\lor B\equiv \neg A \to B$ and $\neg \neg A \equiv A$, your formula

$((p\lor q)\land (\lnot p\lor r))\rightarrow(q\lor r)$

is equivalent to: $$ ((\neg p\to q)\land (p \to r)) \to (\neg q\to r)\text{,} $$ But $(\neg p\to q) \equiv (\neg q\to p)$, so the above formula is equivalent to: $$ ((\neg q\to p)\land (p \to r)) \to (\neg q\to r)\text{.} $$ This should be straightforward to prove. Details on request.


Here is a proof of the resolution inference rule using a Fitch-style proof checker and introduction and elimination rules:

enter image description here

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.