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

Answer 2

One way to show the validity of the rule consists in assuming it invalid, since all rules of inference are either valid or invalid. Then there exists some valuation of the variables such that all of the premises hold, but the conclusion does not.

So, suppose that. Then the conclusion (A $\lor$ C) is false. So, A must be false and so must C. Since (A $\lor$ B) holds true, and A is false, B must hold true. Since ($\lnot$B $\lor$ C) holds truee, and C is false, then $\lnot$B is true also. But, now we have that $\lnot$B and B both hold true. This is not possible. Thus, the assumption of invalidity of the rule has lead to a contradiction. Consequently, the rule of inference is valid.

Mauro has some other methods which work well in his answer.