4
$\begingroup$

The propositional proof system $k$-DNF-resolution, a.k.a. $Res(k)$, is a generalization of propositional resolution, where the lines in a proof are $k$-DNF formulas, i.e., disjunctions of $k$-terms of the form $(a_1 \land \ldots \land a_m)$ with $m\leq k$ and literals $a_i$.

The rules are

  • Weakening: from $C$ infer $C\lor T$,
  • $\land$-introduction: from $C\lor T_1$ and $D\lor T_2$ infer $C\lor D \lor (T_1\land T_2)$,
  • cut: from $C \lor T$ and $D\lor \bar{T}$ infer $C\lor D$,

where $C$ and $D$ are $k$-DNF formulas, $T$ is a $k$-term, and $T_1$ and $T_2$ are $k$-terms such that $(T_1\land T_2)$ is still a $k$-term. $\bar{T}$ denotes the negation of $T$ written as a $k$-clause.

In tree-like resolution, the addition of tautological axioms $x\lor\bar{x}$ is easily seen to be redundant. If $Taut(F)$ denotes the set of these axioms for all variables $x$ in $F$, then this means more precisely:

$F + Taut(F)$ has a tree-like resolution refutation of size $s$ iff $F$ has a tree-like resolution refutation of size $s$.

Now let $Taut_k(F)$ denote the set of all tautologies of the form $T \lor \bar{T}$, for $k$-terms $T$ over the variables of $F$. I think the analogous statement for tree-like $Res(k)$ also holds, and that I can prove it:

$F + Taut_k(F)$ has a tree-like $Res(k)$-refutation of size $s$ iff $F$ has a tree-like $Res(k)$-refutation of size $s$.

Is this fact known, and if so, does it appear somewhere in the literature?

$\endgroup$

1 Answer 1

1
$\begingroup$

Since I could not find a proof in the literature, I wrote a short note containing the proof.

$\endgroup$

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.