# Proving resolution inference rule without truth table

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?

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 :

$(p∨q)∧(¬p∨r)$

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$.

• this was super easy
– Maha
Dec 26, 2015 at 15:45
• @Mauro ALLEGRANZA, but isn't that an equivalence in itself? Jul 18, 2017 at 14:03
• @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. Jul 18, 2017 at 14:06
• @MauroALLEGRANZA, How come? What's the difference? 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:

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