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?
