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?
$\endgroup$3 Answers
$\begingroup$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$.
$\endgroup$ 4 $\begingroup$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.
$\endgroup$ $\begingroup$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
$\endgroup$
