Lower bounds to the size of constant-depth propositional proofs
From MaRDI portal
Publication:4292593
DOI10.2307/2275250zbMath0798.03056OpenAlexW2114817374MaRDI 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 logicpropositional calculuspigeonhole principleFrege systemGentzen sequent calculuslengths of proofs
Complexity of computation (including implicit computational complexity) (03D15) Structure of proofs (03F07) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15) Complexity of proofs (03F20)
Related Items
On the Proof Complexity of Paris-Harrington and Off-Diagonal Ramsey Tautologies ⋮ Proofs with monotone cuts ⋮ On the complexity of resolution with bounded conjunctions ⋮ NP search problems in low fragments of bounded arithmetic ⋮ A proper hierarchy of propositional sequent calculi ⋮ A note about \(k\)-DNF resolution ⋮ FRAGMENTS OF APPROXIMATE COUNTING ⋮ Proof complexity in algebraic systems and bounded depth Frege systems with modular counting ⋮ Some consequences of cryptographical conjectures for \(S_2^1\) and EF ⋮ A reduction of proof complexity to computational complexity for 𝐴𝐶⁰[𝑝 Frege systems] ⋮ Collapsing modular counting in bounded arithmetic and constant depth propositional proofs ⋮ Some consequences of cryptographical conjectures for S 2 1 and EF ⋮ The limits of tractability in resolution-based propositional proof systems ⋮ Towards NP-P via proof complexity and search ⋮ A note on propositional proof complexity of some Ramsey-type statements ⋮ Space characterizations of complexity measures and size-space trade-offs in propositional proof systems ⋮ Herbrand complexity and the epsilon calculus with equality ⋮ The complexity of proving that a graph is Ramsey ⋮ On the elimination of quantifier-free cuts ⋮ An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams ⋮ Lifting lower bounds for tree-like proofs ⋮ A new proof of the weak pigeonhole principle ⋮ Tautologies from Pseudo-Random Generators ⋮ Lower bounds for cutting planes proofs with small coefficients ⋮ Lower bounds for resolution and cutting plane proofs and monotone computations ⋮ Exponential Lower Bounds for AC0-Frege Imply Superpolynomial Frege Lower Bounds ⋮ Resolution over linear equations and multilinear proofs ⋮ On the complexity of cutting-plane proofs using split cuts ⋮ The treewidth of proofs ⋮ Polynomial-size Frege and resolution proofs of \(st\)-connectivity and Hex tautologies ⋮ The Complexity of Propositional Proofs ⋮ Examining Fragments of the Quantified Propositional Calculus ⋮ Short propositional refutations for dense random 3CNF formulas ⋮ How many times do we need an assumption to prove a tautology in minimal logic? Examples on the compression power of classical reasoning ⋮ Proof Complexity of Non-classical Logics ⋮ Satisfiability via Smooth Pictures ⋮ Propositional proof complexity ⋮ On transformations of constant depth propositional proofs ⋮ Some applications of propositional logic to cellular automata ⋮ Tractability of cut-free Gentzen-type propositional calculus with permutation inference. II ⋮ Relative efficiency of propositional proof systems: Resolution vs. cut-free LK ⋮ Separation results for the size of constant-depth propositional proofs
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
This page was built for publication: Lower bounds to the size of constant-depth propositional proofs
