# Resolution on weakening rule by derived clause

How to prove that every clause that is implied by the input formula (learned or not) can be derived using resolution with weakening rule:

$$\frac{C} {C \vee D}$$

(A clause $$C$$ is implied by $$F$$ if for all possible assignments $$A$$ it holds that $$F[A]\implies C[A]$$.)

Alternatively, you can reduce it to plain completeness. One way is as follows. Assume a clause $$C=l_1\lor\dots\lor l_k$$ is implied by a CNF $$F$$. Then the CNF $$F\land\let\ob\overline\ob{l_1}\land\dots\land\ob{l_k}$$ is unsatisfiable, hence it has a resolution refutation. The only way one of the new axioms $$\ob{l_i}$$ can be used in the refutation is in a resolution step $$\dfrac{D\lor l_i\qquad\ob{l_i}}D.$$ So if you just omit these steps along with the $$\ob{l_i}$$ axioms, and perform the remaining inferences as before, you will end up with a valid resolution derivation from $$F$$ that differs from the original one only in that some extra literals from $$C$$ are included in some of the clauses. In particular, the derivation ends with a subclause of $$C$$, from which you can infer $$C$$ by weakening.
• Some literals that belong to $C$ are added to some clauses in the derivation. For example, if I skip the resolution inference $D\lor l_i,\overline{l_i}\mathrel/D$ as written in the answer, then an extra $l_i$ will be included in each clause that's below $D$ in the proof. Commented Feb 27 at 18:08