The complexity of treelike systems over λ-local formulae

We describe a system LK(c[λ]) for refuting CNF formulae, as a restriction of the sequent calculus in which every formula in a sequent is defined over at most λ variables. This further generalizes the system Res(k), a generalization of Resolution to k-DNF introduced in (Krajicek, 2001). We adapt the Pudlak-Impagliazzo game (Pudlak and Impagliazzo, 2000) to prove lower bounds for treelike LK(c[λ]). We show that dynamic satisfiability, which was introduced in (Esteban et al., 2002) to study resolution space complexity, is a sufficient "but not necessary" condition to obtain exponential lower bounds.