| Popis: |
We describe a system LK(c[/spl lambda/]) for refuting CNF formulae, as a restriction of the sequent calculus in which every formula in a sequent is defined over at most /spl lambda/ 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[/spl lambda/]). 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. |
