The k-DNF resolution proof systems are a family of systems indexed by
the integer k, where the kth member is restricted to operating with
formulas in disjunctive normal form with all terms of bounded arity k
(k-DNF formulas). This family was introduced in [Krajicek 2001] as an
extension of the well-studied resolution proof system. A number of
lower bounds have been proven on k-DNF resolution proof length and
space, and it has also been shown that (k+1)-DNF resolution is
exponentially more powerful than k-DNF resolution for all k with
respect to length. For proof space, however, no corresponding
hierarchy has been known except for the (very weak) subsystems
restricted to tree-like proofs. In this work, we establish a strict
space hierarchy for the general, unrestricted k-DNF resolution proof
systems.

This report has been subsumed

We have merged and updated our two ECCC technical reports TR09-034 and TR09-047, and published them as a new ECCC report TR10-125. (An identical version of the new report has also been posted to ArXiv.)

This new paper subsumes the previous two papers.