An exponential lower bound to the size of bounded depth frege proofs of the pigeonhole principle

DOI10.1002/rsa.3240070103zbMath0843.03032OpenAlexW2169713712WikidataQ106785131 ScholiaQ106785131MaRDI QIDQ4847394

Alan R. Woods, Pavel Pudlák, Jan Krajíček

Publication date: 5 November 1995

Published in: Random Structures & Algorithms (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1002/rsa.3240070103

zbMATH Keywords

propositional calculus probabilistic combinatorics proof length pigeonhole principle Frege system depth of proof

Mathematics Subject Classification ID

Combinatorial probability (60C05) Complexity of computation (including implicit computational complexity) (03D15) Classical propositional logic (03B05) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Complexity of proofs (03F20)

Related Items

Combinatorics with Definable Sets: Euler Characteristics and Grothendieck Rings ⋮ Approximate counting and NP search problems ⋮ Unnamed Item ⋮ Approximate Euler characteristic, dimension, and weak pigeonhole principles ⋮ Some remarks on lengths of propositional proofs ⋮ Simplified lower bounds for propositional proofs ⋮ Proof complexity in algebraic systems and bounded depth Frege systems with modular counting ⋮ \(\text{Count}(q)\) does not imply \(\text{Count}(p)\) ⋮ Characterizing Propositional Proofs as Noncommutative Formulas ⋮ An exponential separation between the parity principle and the pigeonhole principle ⋮ A reduction of proof complexity to computational complexity for 𝐴𝐶⁰[𝑝 Frege systems] ⋮ Unnamed Item ⋮ Towards NP-P via proof complexity and search ⋮ Circular (Yet Sound) Proofs in Propositional Logic ⋮ Improved bounds on the weak pigeonhole principle and infinitely many primes from weaker axioms ⋮ Algebraic proof systems over formulas. ⋮ A note on propositional proof complexity of some Ramsey-type statements ⋮ Unnamed Item ⋮ Algebraic proofs over noncommutative formulas ⋮ Higher complexity search problems for bounded arithmetic and a formalized no-gap theorem ⋮ Proof Complexity Meets Algebra ⋮ Forcing in Finite Structures ⋮ Lifting lower bounds for tree-like proofs ⋮ A new proof of the weak pigeonhole principle ⋮ On meta complexity of propositional formulas and propositional proofs ⋮ Parameterized Bounded-Depth Frege Is Not Optimal ⋮ Where pigeonhole principles meet Koenig lemmas ⋮ A form of feasible interpolation for constant depth Frege systems ⋮ Partially definable forcing and bounded arithmetic ⋮ An unexpected separation result in Linearly Bounded Arithmetic ⋮ Unnamed Item ⋮ Polynomial-size Frege and resolution proofs of \(st\)-connectivity and Hex tautologies ⋮ The Complexity of Propositional Proofs ⋮ Resolution with counting: dag-like lower bounds and different moduli ⋮ On the correspondence between arithmetic theories and propositional proof systems – a survey ⋮ Proof Complexity of Non-classical Logics ⋮ Satisfiability via Smooth Pictures ⋮ Propositional proof complexity ⋮ On transformations of constant depth propositional proofs ⋮ Random resolution refutations ⋮ Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs ⋮ Unnamed Item ⋮ Separation results for the size of constant-depth propositional proofs ⋮ LOWER BOUNDS FOR DNF-REFUTATIONS OF A RELATIVIZED WEAK PIGEONHOLE PRINCIPLE ⋮ Bounded-depth Frege complexity of Tseitin formulas for all graphs ⋮ Witnessing functions in bounded arithmetic and search problems ⋮ Reflections on Proof Complexity and Counting Principles

Cites Work