The Complexity of Propositional Proofs
From MaRDI portal
Recommendations
Cites work
- \(\text{Count}(q)\) does not imply \(\text{Count}(p)\)
- A Computing Procedure for Quantification Theory
- A lower bound for the complexity of Craig's interpolants in sentential logic
- A machine program for theorem-proving
- A new proof of the weak pigeonhole principle
- A Switching Lemma for Small Restrictions and Lower Bounds for k-DNF Resolution
- An accurate and scalable collaborative recommender
- An exponential lower bound to the size of bounded depth frege proofs of the pigeonhole principle
- An overview of backtrack search satisfiability algorithms
- Bounded arithmetic, proof complexity and two papers of Parikh
- Cones of Matrices and Set-Functions and 0–1 Optimization
- Constant-depth Frege systems with counting axioms polynomially simulate Nullstellensatz refutations
- Edmonds polytopes and a hierarchy of combinatorial problems. (Reprint)
- Existence and feasibility in arithmetic
- Expander graphs and their applications
- Exponential lower bounds for the pigeonhole principle
- Exponential Lower Bounds on the Lengths of Some Classes of Branch-and-Cut Proofs
- Exponential separation between Res(k) and Res(k+1) for k n
- Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis
- Good degree bounds on Nullstellensatz refutations of the induction principle
- Hiding propositional constants in BDDs.
- Homogenization and the polynomial calculus
- scientific article; zbMATH DE number 4059391 (Why is no real title available?)
- scientific article; zbMATH DE number 1226875 (Why is no real title available?)
- scientific article; zbMATH DE number 1082100 (Why is no real title available?)
- scientific article; zbMATH DE number 2150283 (Why is no real title available?)
- scientific article; zbMATH DE number 819737 (Why is no real title available?)
- scientific article; zbMATH DE number 227056 (Why is no real title available?)
- Improved bounds on the weak pigeonhole principle and infinitely many primes from weaker axioms
- Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
- Linear gaps between degrees for the polynomial calculus modulo distinct primes
- Linear-size constant-depth polylog-threshold circuits
- Lower bounds for cutting planes proofs with small coefficients
- Lower bounds for resolution and cutting plane proofs and monotone computations
- Lower bounds for the polynomial calculus
- Lower bounds for the polynomial calculus and the Gröbner basis algorithm
- Lower bounds for the weak pigeonhole principle and random formulas beyond resolution
- Lower bounds to the size of constant-depth propositional proofs
- Many hard examples for resolution
- Near optimal seperation of tree-like and general resolution
- On Interpolation and Automatization for Frege Systems
- On the automatizability of resolution and related propositional proof systems
- On the complexity of resolution with bounded conjunctions
- On the relative complexity of resolution refinements and cutting planes proof systems
- On the weak pigeonhole principle
- Optimal proof systems imply complete sets for promise classes
- Outline of an algorithm for integer solutions to linear programs
- Polynomial size proofs of the propositional pigeonhole principle
- Propositional consistency proofs
- Propositional proof systems, the consistency of first order theories and the complexity of computations
- Provability of the pigeonhole principle and the existence of infinitely many primes
- Rank bounds and integrality gaps for cutting planes procedures
- Resolution cannot polynomially simulate compressed-BFS
- Resolution lower bounds for perfect matching principles
- Resolution lower bounds for the weak pigeonhole principle
- Sharp thresholds of graph properties, and the k-sat problem
- Short proofs are narrow—resolution made simple
- Some consequences of cryptographical conjectures for \(S_2^1\) and EF
- Space bounds for resolution
- Space Complexity in Propositional Calculus
- The complexity of the pigeonhole principle
- The efficiency of resolution and Davis-Putnam procedures
- The intractability of resolution
- The proof complexity of linear algebra
- The relative efficiency of propositional proof systems
Cited in
(99)- The complexity of Gentzen systems for propositional logic
- Simplified lower bounds for propositional proofs
- Proof complexity in algebraic systems and bounded depth Frege systems with modular counting
- Short proofs of the Kneser-Lovász coloring principle
- A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games
- Cliques enumeration and tree-like resolution proofs
- Understanding cutting planes for QBFs
- On the automatizability of resolution and related propositional proof systems
- Improved algorithms for optimal length resolution refutation in difference constraint systems
- Lower bound techniques for QBF expansion
- The treewidth of proofs
- From truth degree comparison games to sequents-of-relations calculi for Gödel logic
- Partially definable forcing and bounded arithmetic
- The complexity of the Hajós calculus for planar graphs
- Limitations of restricted branching in clause learning
- Strong extension-free proof systems
- Normality, non-contamination and logical depth in classical natural deduction
- On transformations of constant depth propositional proofs
- Quasipolynomial size proofs of the propositional pigeonhole principle
- The universe of propositional approximations
- A game characterisation of tree-like Q-resolution size
- Upper bounds on complexity of Frege proofs with limited use of certain schemata
- On the complexity of the reflected logic of proofs
- A simple proof of QBF hardness
- A game characterisation of tree-like Q-resolution size
- Lifting QBF resolution calculi to DQBF
- Expressing versus proving: relating forms of complexity in logic
- On the complexity of proof deskolemization
- On extracting computations from propositional proofs (a survey)
- Space complexity in polynomial calculus
- On the computational complexity of read once resolution decidability in 2CNF formulas
- Proof complexity and textual cohesion
- Proof Complexity and the Kneser-Lovász Theorem
- Propositional proofs in Frege and extended Frege systems (abstract)
- scientific article; zbMATH DE number 7228403 (Why is no real title available?)
- The complexity of analytic tableaux
- Short proofs of the Kneser-Lovász coloring principle
- Introduction to Donaldson-Thomas and stable pair invariants
- Logical Closure Properties of Propositional Proof Systems
- Twelve Problems in Proof Complexity
- Complexity of propositional proofs (invited talk)
- From feasible proofs to feasible computations
- Propositional Logic for Circuit Classes
- scientific article; zbMATH DE number 125484 (Why is no real title available?)
- Towards NP-P via proof complexity and search
- scientific article; zbMATH DE number 1342249 (Why is no real title available?)
- scientific article; zbMATH DE number 1059248 (Why is no real title available?)
- scientific article; zbMATH DE number 1163984 (Why is no real title available?)
- scientific article; zbMATH DE number 1179974 (Why is no real title available?)
- DEHN FUNCTION AND LENGTH OF PROOFS
- scientific article; zbMATH DE number 2079024 (Why is no real title available?)
- A finite-model-theoretic view on propositional proof complexity
- Efficient reduction of nondeterministic automata with application to language inclusion testing
- scientific article; zbMATH DE number 7029312 (Why is no real title available?)
- Proof Complexity
- scientific article; zbMATH DE number 4114609 (Why is no real title available?)
- scientific article; zbMATH DE number 1860652 (Why is no real title available?)
- scientific article; zbMATH DE number 1860672 (Why is no real title available?)
- scientific article; zbMATH DE number 2102736 (Why is no real title available?)
- scientific article; zbMATH DE number 849963 (Why is no real title available?)
- scientific article; zbMATH DE number 910748 (Why is no real title available?)
- scientific article; zbMATH DE number 1390276 (Why is no real title available?)
- Rank bounds for a hierarchy of Lovász and Schrijver
- Size, cost and capacity: a semantic technique for hard random QBFs
- Substitution and Propositional Proof Complexity
- Reflections on Proof Complexity and Counting Principles
- INFORMATION IN PROPOSITIONAL PROOFS AND ALGORITHMIC PROOF SEARCH
- An Introduction to Lower Bounds on Resolution Proof Systems
- scientific article; zbMATH DE number 7278086 (Why is no real title available?)
- The complexity of finding read-once NAE-resolution refutations
- Short Proofs for the Determinant Identities
- Logical foundations of proof complexity
- The complexity of resolution refinements
- Lower bounds for DNF-refutations of a relativized weak pigeonhole principle
- Present and Future of Practical SAT Solving
- scientific article; zbMATH DE number 3313427 (Why is no real title available?)
- scientific article; zbMATH DE number 2212138 (Why is no real title available?)
- The Complexity of Propositional Proofs with the Substitution Rule
- A note on the complexity of propositional Hoare logic
- PROOF COMPLEXITIES ON A CLASS OF BALANCED FORMULAS IN SOME PROPOSITIONAL SYSTEMS
- Hardness Characterisations and Size-width Lower Bounds for QBF Resolution
- Proof complexity of non-classical logics
- Logical Approaches to Computational Barriers
- Complexity of Null- and Positivstellensatz proofs
- Propositional proof complexity
- Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
- The depth of resolution proofs
- Classes of hard formulas for QBF resolution
- Proving the infeasibility of Horn formulas through read-once resolution
- The relative strength of \#SAT proof systems
- Combinatorics of first order structures and propositional proof systems
- Understanding the relative strength of QBF CDCL solvers and QBF resolution
- Extending merge resolution to a family of QBF-proof systems
- Symmetric proofs in the ideal proof system
- The relative strength of \#SAT proof systems
- Proof complexity of modal resolution
- Optimal length resolution refutations of difference constraint systems
- Symbolic techniques in satisfiability solving
- On meta complexity of propositional formulas and propositional proofs
This page was built for publication: The Complexity of Propositional Proofs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5444711)
