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 DNFs with small conjunctions. 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: 1. The 2n to n weak pigeonhole principle requires exponential size to refute in Res(k), for k ≤ √(log 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.