1
$\begingroup$

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

$\endgroup$
0

1 Answer 1

2
$\begingroup$

What proof of the completeness of resolution do you know? Chances are it can be easily adapted to this more general setting.

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.

$\endgroup$
1
  • 1
    $\begingroup$ 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. $\endgroup$ Commented Feb 27 at 18:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.