On the automatizability of resolution and related propositional proof systems
From MaRDI portal
Publication:1881219
DOI10.1016/j.ic.2003.10.004zbMath1051.03014OpenAlexW2049645218WikidataQ60512211 ScholiaQ60512211MaRDI QIDQ1881219
Albert Atserias, Maria Luisa Bonet
Publication date: 4 October 2004
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.ic.2003.10.004
Related Items (15)
Exponential separation between Res(\(k\)) and Res(\(k+1\)) for \(k \leqslant \varepsilon\log n\) ⋮ Logical Closure Properties of Propositional Proof Systems ⋮ Parity Games and Propositional Proofs ⋮ Optimal length cutting plane refutations of integer programs ⋮ Satisfiability, branch-width and Tseitin tautologies ⋮ A note on SAT algorithms and proof complexity ⋮ On the automatizability of polynomial calculus ⋮ Finding the Hardest Formulas for Resolution ⋮ Automatizability and Simple Stochastic Games ⋮ On Minimal Unsatisfiability and Time-Space Trade-offs for k-DNF Resolution ⋮ A combinatorial characterization of resolution width ⋮ Mean-payoff games and propositional proofs ⋮ Unnamed Item ⋮ The Complexity of Propositional Proofs ⋮ Resolution for Max-SAT
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Near optimal seperation of tree-like and general resolution
- The monotone circuit complexity of Boolean functions
- An exponential lower bound for the size of monotone real circuits
- Some consequences of cryptographical conjectures for \(S_2^1\) and EF
- On reducibility and symmetry of disjoint NP pairs.
- Optimality of size-width tradeoffs for resolution
- Non-automatizability of bounded-depth Frege proofs
- Lower bounds for the weak pigeonhole principle and random formulas beyond resolution
- On the Relative Complexity of Resolution Refinements and Cutting Planes Proof Systems
- Minimum propositional proof length is NP-hard to linearly approximate
- On the weak pigeonhole principle
- Resolution Is Not Automatizable Unless W[P Is Tractable]
- The relative efficiency of propositional proof systems
- 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
- Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- A new proof of the weak pigeonhole principle
This page was built for publication: On the automatizability of resolution and related propositional proof systems
