Lower bounds to the size of constant-depth propositional proofs
From MaRDI portal
Publication:4292593
Recommendations
Cites work
- Bounds for proof-search and speed-up in the predicate calculus
- Proof theory
- Provability of the pigeonhole principle and the existence of infinitely many primes
- 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
Cited in
(57)- 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
- A note about k-DNF resolution
- On the complexity of resolution with bounded conjunctions
- The treewidth of proofs
- On transformations of constant depth propositional proofs
- 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
- Minimum propositional proof length is NP-hard to linearly approximate
- 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 \(\mathrm{AC}^{0}\)-Frege imply superpolynomial Frege lower bounds
- Examining Fragments of the Quantified Propositional Calculus
- Some applications of propositional logic to cellular automata
- The limits of tractability in resolution-based propositional proof systems
- Towards NP-P via proof complexity and search
- Lower bounds for cutting planes proofs with small coefficients
- Lower bounds for resolution and cutting plane proofs and monotone computations
- scientific article; zbMATH DE number 1114022 (Why is no real title available?)
- Some subsystems of constant-depth Frege with parity
- Near-Optimal Lower Bounds on Quantifier Depth and Weisfeiler--Leman Refinement Steps
- Lifting lower bounds for tree-like proofs
- Short refutations for an equivalence-chain principle for constant-depth formulas
- On the proof complexity of Paris-Harrington and off-diagonal Ramsey tautologies
- 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
- Some consequences of cryptographical conjectures for S 2 1 and EF
- Propositional proof complexity
- Space characterizations of complexity measures and size-space trade-offs in propositional proof systems
- Herbrand complexity and the epsilon calculus with equality
- A note on propositional proof complexity of some Ramsey-type statements
- On the elimination of quantifier-free cuts
- Proving the infeasibility of Horn formulas through read-once resolution
- First-order reasoning and efficient semi-algebraic proofs
- On the strength of Sherali-Adams and Nullstellensatz as propositional proof systems
- Failure of feasible disjunction property for k-DNF resolution and NP-hardness of automating it
- Depth-d Frege systems are not automatable unless P\,=\,NP
- From proof complexity to circuit complexity via interactive protocols
- On the completeness of interpolation algorithms
- On protocols for monotone feasible interpolation
- Strength and limitations of Sherali-Adams and nullstellensatz proof systems
- Prover-adversary games for systems over (non-deterministic) branching programs
- Completeness of interpolation algorithms in classical and non-classical logics
- 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
This page was built for publication: Lower bounds to the size of constant-depth propositional proofs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4292593)
