Lower bounds to the size of constant-depth propositional proofs
From MaRDI portal
Publication:4292593
DOI10.2307/2275250zbMath0798.03056MaRDI QIDQ4292593
Publication date: 3 November 1994
Published in: Journal of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2307/2275250
propositional logic; propositional calculus; pigeonhole principle; Frege system; Gentzen sequent calculus; lengths of proofs
03D15: Complexity of computation (including implicit computational complexity)
03F07: Structure of proofs
68Q15: Complexity classes (hierarchies, relations among complexity classes, etc.)
03F20: Complexity of proofs
Related Items
Lower bounds for cutting planes proofs with small coefficients, Lower bounds for resolution and cutting plane proofs and monotone computations, NP search problems in low fragments of bounded arithmetic, An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams, The Complexity of Propositional Proofs, A new proof of the weak pigeonhole principle, Proof Complexity of Non-classical Logics, The limits of tractability in resolution-based propositional proof systems, Towards NP-P via proof complexity and search, Lifting lower bounds for tree-like proofs, A note on propositional proof complexity of some Ramsey-type statements, On the elimination of quantifier-free cuts, Short propositional refutations for dense random 3CNF formulas, Resolution over linear equations and multilinear proofs, On the complexity of cutting-plane proofs using split cuts, A proper hierarchy of propositional sequent calculi, Proof complexity in algebraic systems and bounded depth Frege systems with modular counting, Some consequences of cryptographical conjectures for \(S_2^1\) and EF, Tractability of cut-free Gentzen-type propositional calculus with permutation inference. II, Relative efficiency of propositional proof systems: Resolution vs. cut-free LK, On the complexity of resolution with bounded conjunctions, Polynomial-size Frege and resolution proofs of \(st\)-connectivity and Hex tautologies, How many times do we need an assumption to prove a tautology in minimal logic? Examples on the compression power of classical reasoning, Separation results for the size of constant-depth propositional proofs, Tautologies from Pseudo-Random Generators, Satisfiability via Smooth Pictures, Proofs with monotone cuts, FRAGMENTS OF APPROXIMATE COUNTING, A reduction of proof complexity to computational complexity for 𝐴𝐶⁰[𝑝 Frege systems], Collapsing modular counting in bounded arithmetic and constant depth propositional proofs, Exponential Lower Bounds for AC0-Frege Imply Superpolynomial Frege Lower Bounds, Examining Fragments of the Quantified Propositional Calculus, Some applications of propositional logic to cellular automata
Cites Work
- Resolution proofs of generalized pigeonhole principles
- The intractability of resolution
- The syntax and semantics of infinitary languages
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Bounds for proof-search and speed-up in the predicate calculus
- Provability of the pigeonhole principle and the existence of infinitely many primes
- Proof theory
