Non-automatizability of bounded-depth Frege proofs
From MaRDI portal
Publication:1764155
DOI10.1007/s00037-004-0183-5zbMath1058.03063OpenAlexW3014805183WikidataQ60512205 ScholiaQ60512205MaRDI QIDQ1764155
Carlos Domingo, Toniann Pitassi, Maria Luisa Bonet, Ricard Gavaldà, Alexis Maciel
Publication date: 23 February 2005
Published in: Computational Complexity (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00037-004-0183-5
Mechanization of proofs and logical operations (03B35) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Complexity of proofs (03F20)
Related Items
On the automatizability of resolution and related propositional proof systems ⋮ Nondeterministic functions and the existence of optimal proof systems ⋮ Feasible Interpolation for QBF Resolution Calculi ⋮ Classes of representable disjoint \textsf{NP}-pairs ⋮ Parity Games and Propositional Proofs ⋮ Towards NP-P via proof complexity and search ⋮ On the automatizability of polynomial calculus ⋮ The canonical pairs of bounded depth Frege systems ⋮ Lifting lower bounds for tree-like proofs ⋮ Exponential Lower Bounds for AC0-Frege Imply Superpolynomial Frege Lower Bounds ⋮ A form of feasible interpolation for constant depth Frege systems ⋮ Mean-payoff games and propositional proofs ⋮ Understanding cutting planes for QBFs ⋮ Short Proofs Are Hard to Find
