binary resolution rule proof

Question

I want to proof the binary resolution rule that is, if we For any two clauses $C_1$ and $C_2$, if there is a literal $L_1$ in $C_1$ that is complementary to a literal $L_2$ in $C_2$, then delete $L_1$ and $L_2$ from $C_1$ and $C_2$ respectively, and construct the disjunction of the remaining clauses. The constructed clause is a resolvent of $C_1$ and $C_2$

It is seen as follows

$$A \vee B, \space \space ¬B \vee C$$ $$ ----------$$ $$A \vee C$$

How would I proof this rule, Do I go by truth table or is there a normal way to prove this !

Answer 1

The Resolution rule is the rule of inference :

$$\frac {a \lor b \quad \quad \lnot b \lor c} {a \lor c}.$$

As any other inference rule, the rule is sound, i.e. the premises must entail the conclusion.

You can prove this via truth table, or with an equivalent "semantic" argument :

due to the fact that $b$ and $\lnot b$ cannot both be true, the truth of the two premises means that at least one of $a$ and $c$ must be true, and this is enough to conclude that $a \lor c$ must be true.

---

Another way to show the soundness of the rule is to exploit the equivalence between : $p \to q$ and $\lnot p \to q$. Thus, the rule can be rewritten as :

$$\frac {\lnot a \to b \quad \quad b \to c} {\lnot a \to c}.$$

---

You can consider a simplified case of Resolution (also called : modus ponens) :

$$\frac {b \quad \quad \lnot b \lor c} {c}.$$

This rule is based on the tautology :

$(b \land (\lnot b \lor c)) \to c$.

By distributivity the antecedent is equivalent to : $(b \land \lnot b) \lor (b \land c) \equiv (b \land c)$.

Thus we can simplify the above tautology to : $(b \land c) \to c$.