The Complexity of Propositional Proofs
From MaRDI portal
Publication:5444711
DOI10.2178/bsl/1203350879zbMath1133.03037OpenAlexW1996660205MaRDI QIDQ5444711
Publication date: 25 February 2008
Published in: Bulletin of Symbolic Logic (Search for Journal in Brave)
Full work available at URL: https://projecteuclid.org/euclid.bsl/1203350879
Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Complexity of proofs (03F20)
Related Items (48)
Hardness Characterisations and Size-width Lower Bounds for QBF Resolution ⋮ Proof complexity of modal resolution ⋮ Short Proofs of the Kneser-Lovász Coloring Principle ⋮ Unnamed Item ⋮ Optimal length resolution refutations of difference constraint systems ⋮ Short proofs of the Kneser-Lovász coloring principle ⋮ Introduction to Donaldson–Thomas and Stable Pair Invariants ⋮ Symbolic techniques in satisfiability solving ⋮ Propositional Proofs in Frege and Extended Frege Systems (Abstract) ⋮ A simple proof of QBF hardness ⋮ From truth degree comparison games to sequents-of-relations calculi for Gödel logic ⋮ Proof complexity in algebraic systems and bounded depth Frege systems with modular counting ⋮ A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games ⋮ Space Complexity in Polynomial Calculus ⋮ Unnamed Item ⋮ Towards NP-P via proof complexity and search ⋮ A game characterisation of tree-like Q-resolution size ⋮ Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution ⋮ Improved algorithms for optimal length resolution refutation in difference constraint systems ⋮ Cliques enumeration and tree-like resolution proofs ⋮ The depth of resolution proofs ⋮ An Introduction to Lower Bounds on Resolution Proof Systems ⋮ On the Computational Complexity of Read once Resolution Decidability in 2CNF Formulas ⋮ Rank bounds for a hierarchy of Lovász and Schrijver ⋮ Lower bound techniques for QBF expansion ⋮ Partially definable forcing and bounded arithmetic ⋮ The treewidth of proofs ⋮ The complexity of the Hajós calculus for planar graphs ⋮ Limitations of restricted branching in clause learning ⋮ Understanding cutting planes for QBFs ⋮ The complexity of resolution refinements ⋮ A Game Characterisation of Tree-like Q-resolution Size ⋮ Proof Complexity of Non-classical Logics ⋮ Strong extension-free proof systems ⋮ Lifting QBF Resolution Calculi to DQBF ⋮ Normality, non-contamination and logical depth in classical natural deduction ⋮ The Complexity of Finding Read-Once NAE-Resolution Refutations ⋮ DEHN FUNCTION AND LENGTH OF PROOFS ⋮ Unnamed Item ⋮ The complexity of analytic tableaux ⋮ LOWER BOUNDS FOR DNF-REFUTATIONS OF A RELATIVIZED WEAK PIGEONHOLE PRINCIPLE ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Present and Future of Practical SAT Solving ⋮ Short Proofs for the Determinant Identities ⋮ Quasipolynomial size proofs of the propositional pigeonhole principle ⋮ Reflections on Proof Complexity and Counting Principles
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Near optimal seperation of tree-like and general resolution
- Exponential lower bounds for the pigeonhole principle
- An accurate and scalable collaborative recommender
- Exponential separation between Res(\(k\)) and Res(\(k+1\)) for \(k \leqslant \varepsilon\log n\)
- Hiding propositional constants in BDDs.
- The intractability of resolution
- Propositional consistency proofs
- Linear-size constant-depth polylog-threshold circuits
- Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis
- Good degree bounds on Nullstellensatz refutations of the induction principle
- Lower bounds for the polynomial calculus
- Bounded arithmetic, proof complexity and two papers of Parikh
- The complexity of the pigeonhole principle
- \(\text{Count}(q)\) does not imply \(\text{Count}(p)\)
- Some consequences of cryptographical conjectures for \(S_2^1\) and EF
- Optimal proof systems imply complete sets for promise classes
- Improved bounds on the weak pigeonhole principle and infinitely many primes from weaker axioms
- Homogenization and the polynomial calculus
- Resolution cannot polynomially simulate compressed-BFS
- Space bounds for resolution
- Lower bounds for the weak pigeonhole principle and random formulas beyond resolution
- An overview of backtrack search satisfiability algorithms
- On the automatizability of resolution and related propositional proof systems
- Resolution lower bounds for perfect matching principles
- On the complexity of resolution with bounded conjunctions
- The proof complexity of linear algebra
- Lower bounds for the polynomial calculus and the Gröbner basis algorithm
- Edmonds polytopes and a hierarchy of combinatorial problems. (Reprint)
- On the Relative Complexity of Resolution Refinements and Cutting Planes Proof Systems
- On the weak pigeonhole principle
- The Efficiency of Resolution and Davis--Putnam Procedures
- Space Complexity in Propositional Calculus
- Outline of an algorithm for integer solutions to linear programs
- Propositional proof systems, the consistency of first order theories and the complexity of computations
- Many hard examples for resolution
- Expander graphs and their applications
- Polynomial size proofs of the propositional pigeonhole principle
- Cones of Matrices and Set-Functions and 0–1 Optimization
- The relative efficiency of propositional proof systems
- Provability of the pigeonhole principle and the existence of infinitely many primes
- Sharp thresholds of graph properties, and the $k$-sat problem
- Lower bounds to the size of constant-depth propositional proofs
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Lower bounds for cutting planes proofs with small coefficients
- Lower bounds for resolution and cutting plane proofs and monotone computations
- Short proofs are narrow—resolution made simple
- On Interpolation and Automatization for Frege Systems
- A Switching Lemma for Small Restrictions and Lower Bounds for k-DNF Resolution
- A lower bound for the complexity of Craig's interpolants in sentential logic
- An exponential lower bound to the size of bounded depth frege proofs of the pigeonhole principle
- Constant-depth Frege systems with counting axioms polynomially simulate Nullstellensatz refutations
- Resolution lower bounds for the weak pigeonhole principle
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- Existence and feasibility in arithmetic
- Exponential Lower Bounds on the Lengths of Some Classes of Branch-and-Cut Proofs
- A new proof of the weak pigeonhole principle
- Linear gaps between degrees for the polynomial calculus modulo distinct primes
This page was built for publication: The Complexity of Propositional Proofs
