# Eliminating tautological axioms in tree-like $k$-DNF resolution

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?