Exponential Lower Bounds for AC0-Frege Imply Superpolynomial Frege Lower Bounds

Yuval Filmus, Toniann Pitassi, Rahul Santhanam

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

We give a general transformation that turns polynomial-size Frege proofs into subexponential-size AC0-Frege proofs. This indicates that proving truly exponential lower bounds for AC0-Frege is hard, as it is a long-standing open problem to prove superpolynomial lower bounds for Frege. Our construction is optimal for proofs of formulas of unbounded depth.

As a consequence of our main result, we are able to shed some light on the question of automatizability for bounded-depth Frege systems. First, we present a simpler proof of the results of Bonet et al. showing that under cryptographic assumptions, bounded-depth Frege proofs are not automatizable. Second, we show that because our proof is more general, under the right cryptographic assumptions, it could resolve the automatizability question for lower-depth Frege systems.
Original languageEnglish
Article number5
Number of pages16
JournalACM Transactions on Computation Theory
Issue number2
Publication statusPublished - 11 May 2015

Keywords / Materials (for Non-textual outputs)

  • Proof complexity


Dive into the research topics of 'Exponential Lower Bounds for AC0-Frege Imply Superpolynomial Frege Lower Bounds'. Together they form a unique fingerprint.

Cite this