Pseudorandom generators in propositional proof complexity

We call a pseudorandom generator G(n) : {0, 1}(n) --> {0, 1}(m) hard for a propositional proof system P if P cannot efficiently prove the (properly encoded) statement G(n)(x(1),..., x(n)) not equal b for any string b is an element of{0, 1}(m). We consider a variety of "combinatorial" pseudorandom generators inspired by the Nisan-Wigderson generator on the one hand, and by the construction of Tseitin tautologies on the other. We prove that under certain circumstances these generators are hard for such proof systems as resolution, polynomial calculus, and polynomial calculus with resolution (PCR).