Pseudorandom generators in propositional proof complexity

We call a pseudorandom generator G_n:{0,1}ⁿ→{0,1}^m hard for a propositional proof system P if P can not efficiently prove the (properly encoded) statement G_n(x₁,...,x_n )≠b for any string bε{0,1}^m. We consider a variety of “combinatorial” pseudorandom generators inspired by the Nisan-Wigderson generator on 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)