Exponential lower bounds for AC^0-Frege imply superpolynomial Frege lower bounds

DOI10.1145/2656209MaRDI QIDQ2828228zbMATH OpenOpenAlexFDO

Authors Yuval Filmus, Toniann Pitassi, Rahul Santhanam

Publication date 24 October 2016

Published in ACM Transactions on Computation Theory (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2656209

zbMATH Keywords

proof complexity

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Recommendations

• Exponential lower bounds for \(\mathrm{AC}^{0}\)-Frege imply superpolynomial Frege lower bounds
• Non-automatizability of bounded-depth Frege proofs
• On Interpolation and Automatization for Frege Systems
• Approximation and Small-Depth Frege Proofs
• Hard examples for the bounded depth Frege proof system

Cited in

(4)

• Non-automatizability of bounded-depth Frege proofs
• Theories for subexponential-size bounded-depth Frege proofs
• Exponential lower bounds for \(\mathrm{AC}^{0}\)-Frege imply superpolynomial Frege lower bounds
• A fixed-depth size-hierarchy theorem for AC ⁰ [⊕] via the coin problem

This page was built for publication: Exponential lower bounds for \(\mathrm{AC}^0\)-Frege imply superpolynomial Frege lower bounds

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2828228)