Non-automatizability of bounded-depth Frege proofs

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

zbMATH Keywords

interpolationProof complexityautomatizability of proof systemsFrege proof systems

Mathematics Subject Classification ID

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 (14)

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

This page was built for publication: Non-automatizability of bounded-depth Frege proofs