We prove a new switching lemma that works for restrictions that set only a small fraction of the variables and is applicable to DNFs with small bottom fan-in. We use this to prove lower bounds for the Res(k) propositional proof system, an extension of resolution whose lines are k-DNFs instead of clauses. We also obtain an exponential separation between depth d circuits of bottom fan-in k and depth d circuits of bottom fan-in k+1.

Our results for Res(k) proofs are:

1. The 2n to n weak pigeonhole principle requires exponential size to refute in Res(k), for k up to a power of log n.
2. For each constant k, there exists a constant w>k so that random w-CNFs require exponential size to refute in Res(k).
3. For each constant k, there are sets of clauses which have polynomial size Res(k+1) refutations, but which require exponential size Res(k) refutations.

This is joint work with Nathan Segerlind and Samuel Buss.

In principle this talk will be self-contained; I will review needed definitions concerning boolean formulas and resolution.