The Community for Technology Leaders
Proceedings 41st Annual Symposium on Foundations of Computer Science (2000)
Redondo Beach, California
Nov. 12, 2000 to Nov. 14, 2000
ISSN: 0272-5428
ISBN: 0-7695-0850-2
pp: 43
M. Alekhnovich , Moscow State Univ., Russia
E. Ben-Sasson , Moscow State Univ., Russia
A.A. Razborov , Moscow State Univ., Russia
A. Wigderson , Moscow State Univ., Russia
We call a pseudorandom generator G/sub n/:{0,1}/sup n//spl rarr/{0,1}/sup m/ hard for a propositional proof system P if P can not efficiently prove the (properly encoded) statement G/sub n/(x/sub 1/,...,x/sub n/)/spl ne/b for any string b/spl epsiv/{0,1}/sup 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).
theorem proving; computational complexity; process algebra; random processes; pseudorandom generators; propositional proof complexity; combinatorial pseudorandom generators; Nisan-Wigderson generator; Tseitin tautologies; resolution; polynomial calculus with resolution; polynomial calculus

A. Razborov, E. Ben-Sasson, A. Wigderson and M. Alekhnovich, "Pseudorandom generators in propositional proof complexity," Proceedings 41st Annual Symposium on Foundations of Computer Science(FOCS), Redondo Beach, California, 2000, pp. 43.
91 ms
(Ver 3.3 (11022016))