A characterization of tree-like resolution size

DOI10.1016/J.IPL.2013.06.002MaRDI QIDQ2444907zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Olaf Beyersdorff, Nicola Galesi, Massimo Lauria

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 complexityproof complexityProver-Delayer gamesresolution

Mathematics Subject Classification ID

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

Recommendations

• A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games
• A game characterisation of tree-like Q-resolution size
• A game characterisation of tree-like Q-resolution size
• A combinatorial characterization of treelike resolution space
• Game Characterizations and the PSPACE-Completeness of Tree Resolution Space

Cites work

• A combinatorial characterization of treelike resolution space
• A Computing Procedure for Quantification Theory
• A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games
• A Machine-Oriented Logic Based on the Resolution Principle
• scientific article; zbMATH DE number 1522926 (Why is no real title available?)
• scientific article; zbMATH DE number 1445296 (Why is no real title available?)
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Near optimal seperation of tree-like and general resolution
• Parameterized complexity of DPLL search procedures
• Proofs as Games
• Short proofs are narrow—resolution made simple
• Space bounds for resolution
• The intractability of resolution

Cited in

(20)

• A note about k-DNF resolution
• A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games
• Cliques enumeration and tree-like resolution proofs
• On semantic cutting planes with very small coefficients
• Lower bound techniques for QBF expansion
• A game characterisation of tree-like Q-resolution size
• A game characterisation of tree-like Q-resolution size
• A tutorial on time and space bounds in tree-like resolution
• scientific article; zbMATH DE number 7228403 (Why is no real title available?)
• Game Characterizations and the PSPACE-Completeness of Tree Resolution Space
• Relativization makes contradictions harder for resolution
• Efficient reduction of nondeterministic automata with application to language inclusion testing
• scientific article; zbMATH DE number 7029312 (Why is no real title available?)
• Size, cost and capacity: a semantic technique for hard random QBFs
• A separator theorem for hypergraphs and a CSP-SAT algorithm
• Near optimal seperation of tree-like and general resolution
• On (simple) decision tree rank
• Pseudo-deterministic query complexity of search problems
• Proof complexity of modal resolution
• Improving resolution width lower bounds for k-CNFs with applications to the strong exponential time hypothesis

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2444907)