A characterization of tree-like resolution size

DOI10.1016/j.ipl.2013.06.002zbMath1285.68058DBLPjournals/ipl/BeyersdorffGL13OpenAlexW2103193591WikidataQ59901843 ScholiaQ59901843MaRDI QIDQ2444907

Olaf Beyersdorff, Massimo Lauria, Nicola Galesi

Publication date: 11 April 2014

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: http://eprints.whiterose.ac.uk/79312/1/prover-delayer.pdf

zbMATH Keywords

computational complexityresolutionproof complexityProver-Delayer games

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) 2-person games (91A05) Applications of game theory (91A80) Complexity of computation (including implicit computational complexity) (03D15) Equational classes, universal algebra in model theory (03C05) Complexity of proofs (03F20)

Related Items (16)

Proof complexity of modal resolution ⋮ Unnamed Item ⋮ A note about \(k\)-DNF resolution ⋮ Relativization makes contradictions harder for resolution ⋮ On (simple) decision tree rank ⋮ Unnamed Item ⋮ Improving resolution width lower bounds for \(k\)-CNFs with applications to the strong exponential time hypothesis ⋮ A game characterisation of tree-like Q-resolution size ⋮ Cliques enumeration and tree-like resolution proofs ⋮ Unnamed Item ⋮ Lower bound techniques for QBF expansion ⋮ On semantic cutting planes with very small coefficients ⋮ A Game Characterisation of Tree-like Q-resolution Size ⋮ A Tutorial on Time and Space Bounds in Tree-Like Resolution ⋮ Unnamed Item ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Near optimal seperation of tree-like and general resolution
• A combinatorial characterization of treelike resolution space
• The intractability of resolution
• A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games
• Space bounds for resolution
• Proofs as Games
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Short proofs are narrow—resolution made simple
• A Machine-Oriented Logic Based on the Resolution Principle
• A Computing Procedure for Quantification Theory
• Parameterized Complexity of DPLL Search Procedures

This page was built for publication: A characterization of tree-like resolution size