A reduction of proof complexity to computational complexity for 𝐴𝐶⁰[𝑝] Frege systems
Jan Krajı́ček · Proceedings of the American Mathematical Society · 2015
We give a general reduction of lengths-of-proofs lower bounds for constant depth Frege systems in DeMorgan language augmented by a connective counting modulo a prime p p (the so-called A C 0 [ p ] AC^0[p] Frege systems) to computational complexity lower bounds for search tasks involving search trees branching upon values of maps on the vector space of low degree polynomials over F p {\textbf {F}_p} .