[Math] Proving resolution inference rule without truth table

first-order-logiclogicpropositional-calculus

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?

Best Answer

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

Related Question