Polynomial size proofs of the propositional pigeonhole principle
From MaRDI portal
Publication:3775553
DOI10.2307/2273826zbMath0636.03053OpenAlexW1968584500MaRDI QIDQ3775553
Publication date: 1987
Published in: Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.92.8201
length of proofpropositional pigeonhole principleexponential speedup over resolutionpolynomial size Frege proofsprovability in theories of bounded arithmetic
First-order arithmetic and fragments (03F30) Classical propositional logic (03B05) Complexity of proofs (03F20)
Related Items (54)
Monotone simulations of non-monotone proofs. ⋮ Proofs with monotone cuts ⋮ A lower bound for tree resolution ⋮ Proof complexity of modal resolution ⋮ The proof complexity of linear algebra ⋮ Short Proofs of the Kneser-Lovász Coloring Principle ⋮ Expander Construction in VNC1 ⋮ Proof compressions with circuit-structured substitutions ⋮ Short proofs of the Kneser-Lovász coloring principle ⋮ ALOGTIME and a conjecture of S. A. Cook ⋮ A modal view on resource-bounded propositional logics ⋮ Some remarks on lengths of propositional proofs ⋮ Propositional Proofs in Frege and Extended Frege Systems (Abstract) ⋮ Cutting planes, connectivity, and threshold logic ⋮ \(\text{Count}(q)\) does not imply \(\text{Count}(p)\) ⋮ A lower bound for intuitionistic logic ⋮ An exponential separation between the parity principle and the pigeonhole principle ⋮ Short resolution proofs for a sequence of tricky formulas ⋮ Expander construction in \(\mathrm{VNC}^1\) ⋮ The power of the binary value principle ⋮ 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. ⋮ Higher complexity search problems for bounded arithmetic and a formalized no-gap theorem ⋮ Resolution proofs of generalized pigeonhole principles ⋮ Towards a Unified Complexity Theory of Total Functions ⋮ Propositional consistency proofs ⋮ A new proof of the weak pigeonhole principle ⋮ A bounded arithmetic AID for Frege systems ⋮ Tractability of cut-free Gentzen type propositional calculus with permutation inference ⋮ Towards a unified complexity theory of total functions ⋮ Exponential Lower Bounds for AC0-Frege Imply Superpolynomial Frege Lower Bounds ⋮ Parameterized Bounded-Depth Frege Is Not Optimal ⋮ Generalisation of proof simulation procedures for Frege systems by M.L. Bonet and S.R. Buss ⋮ Exponential lower bounds for the pigeonhole principle ⋮ Partially definable forcing and bounded arithmetic ⋮ Asymptotic cyclic expansion and bridge groups of formal proofs ⋮ Extension without cut ⋮ Polynomial-size Frege and resolution proofs of \(st\)-connectivity and Hex tautologies ⋮ Understanding cutting planes for QBFs ⋮ The Complexity of Propositional Proofs ⋮ Exploiting Symmetry in SMT Problems ⋮ On the correspondence between arithmetic theories and propositional proof systems – a survey ⋮ Substitution Frege and extended Frege proof systems in non-classical logics ⋮ A Measure of Logical Inference and Its Game Theoretical Applications ⋮ Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs ⋮ Tractability of cut-free Gentzen-type propositional calculus with permutation inference. II ⋮ Bounded-depth Frege complexity of Tseitin formulas for all graphs ⋮ Proof-Theoretic Semantics and Feasibility ⋮ Lower bounds for the weak pigeonhole principle and random formulas beyond resolution ⋮ Quasipolynomial size proofs of the propositional pigeonhole principle ⋮ Simplification in a satisfiability checker for VLSI applications ⋮ Synthetic tableaux: Minimal tableau search heuristics
Cites Work
This page was built for publication: Polynomial size proofs of the propositional pigeonhole principle
