Hard examples for the bounded depth Frege proof system
From MaRDI portal
Publication:1430570
DOI10.1007/s00037-002-0172-5zbMath1043.03043OpenAlexW2075906306MaRDI QIDQ1430570
Publication date: 27 May 2004
Published in: Computational Complexity (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00037-002-0172-5
resolutionproof complexityco-NP completenessexpander graphpropositional proof systemsize of a bounded depth Frege proofTseitin contradictions
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 (max. 100)
Characterizing Tseitin-Formulas with Short Regular Resolution Refutations ⋮ Resolution with counting: dag-like lower bounds and different moduli ⋮ Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs ⋮ Bounded-depth Frege complexity of Tseitin formulas for all graphs ⋮ Resolution over linear equations modulo two ⋮ Reflections on Proof Complexity and Counting Principles ⋮ Characterizing Tseitin-formulas with short regular resolution refutations
This page was built for publication: Hard examples for the bounded depth Frege proof system
