<p>Since I could not find a proof in the literature, I wrote <a href="https://www.tcs.ifi.lmu.de/mitarbeiter/jan-johannsen/publikationen-1/unpubl/tautaxiom.pdf" rel="nofollow noreferrer">a short note</a> containing the proof.</p>

CC BY-SA 4.0
2022-02-28T16:06:14.750Z
2022-02-28T16:06:14.750Z
Jan Johannsen
<p>The propositional proof system <span class="math-container">$k$</span>-DNF-resolution, a.k.a. <span class="math-container">$Res(k)$</span>, is a generalization of propositional resolution, where the lines in a proof are <span class="math-container">$k$</span>-DNF formulas, i.e., disjunctions of <span class="math-container">$k$</span>-terms of the form <span class="math-container">$(a_1 \land \ldots \land a_m)$</span> with <span class="math-container">$m\leq k$</span> and literals <span class="math-container">$a_i$</span>.  </p>

<p>The rules are</p>

<ul>
<li>Weakening: from <span class="math-container">$C$</span> infer <span class="math-container">$C\lor T$</span>,</li>
<li><span class="math-container">$\land$</span>-introduction: from <span class="math-container">$C\lor T_1$</span> and <span class="math-container">$D\lor T_2$</span> infer <span class="math-container">$C\lor D \lor (T_1\land T_2)$</span>,</li>
<li>cut: from <span class="math-container">$C \lor T$</span> and <span class="math-container">$D\lor \bar{T}$</span> infer <span class="math-container">$C\lor D$</span>,</li>
</ul>

<p>where <span class="math-container">$C$</span> and <span class="math-container">$D$</span> are <span class="math-container">$k$</span>-DNF formulas, <span class="math-container">$T$</span> is a <span class="math-container">$k$</span>-term, and <span class="math-container">$T_1$</span> and <span class="math-container">$T_2$</span> are <span class="math-container">$k$</span>-terms such that <span class="math-container">$(T_1\land T_2)$</span> is still a <span class="math-container">$k$</span>-term. <span class="math-container">$\bar{T}$</span> denotes the negation of <span class="math-container">$T$</span> written as a <span class="math-container">$k$</span>-clause. </p>

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

<blockquote>
  <p><span class="math-container">$F + Taut(F)$</span> has a tree-like resolution refutation of size <span class="math-container">$s$</span> iff <span class="math-container">$F$</span> has a  tree-like resolution refutation of size <span class="math-container">$s$</span>. </p>
</blockquote>

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

<blockquote>
  <p><span class="math-container">$F + Taut_k(F)$</span> has a tree-like <span class="math-container">$Res(k)$</span>-refutation of size <span class="math-container">$s$</span> iff <span class="math-container">$F$</span> has a tree-like <span class="math-container">$Res(k)$</span>-refutation of size <span class="math-container">$s$</span>. </p>
</blockquote>

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

<reference-request><proof-complexity><resolution>
Eliminating tautological axioms in tree-like $k$-DNF resolution
Jan Johannsen
# Eliminating tautological axioms in tree-like $k$-DNF resolution

(Asked by: username_0 on 2019-09-26)

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?

**Tags:** reference-request, proof-complexity, resolution


---

## 1 answers

### Answer by username_0 on 2022-02-28. Score: 1 | Accepted answer

Since I could not find a proof in the literature, I wrote [a short note](https://www.tcs.ifi.lmu.de/mitarbeiter/jan-johannsen/publikationen-1/unpubl/tautaxiom.pdf) containing the proof.


---

