A switching lemma for small restrictions and lower bounds for k-DNF resolution

We prove a new switching lemma that works for restrictions that set only a small fraction of the variables and is applicable to formulas in disjunctive normal form (DNFs) with small terms. We use this to prove lower bounds for the Res(k) propositional proof system, an extension of resolution which works with 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) are as follows: 1. The 2n to n weak pigeonhole principle requires exponential size to refute in Res(k) for krootlog n/log 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