A simplified way of proving trade-off results for resolution

DOI10.1016/j.ipl.2009.06.006zbMath1202.68388OpenAlexW2109895531MaRDI QIDQ989569

Jakob Nordström

Publication date: 20 August 2010

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

Full work available at URL: https://doi.org/10.1016/j.ipl.2009.06.006

zbMATH Keywords

computational complexitywidthlengthresolutionproof complexityautomatic theorem provingspacetrade-offs

Mathematics Subject Classification ID

Related Items (8)

From Small Space to Small Width in Resolution ⋮ Space Complexity in Polynomial Calculus ⋮ Contradiction separation based dynamic multi-clause synergized automated deduction ⋮ An Introduction to Lower Bounds on Resolution Proof Systems ⋮ Unnamed Item ⋮ Nullstellensatz size-degree trade-offs from reversible pebbling ⋮ Strong extension-free proof systems ⋮ Time-Space Trade-offs in Resolution: Superpolynomial Lower Bounds for Superlinear Space

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The complexity of facets resolved
• Optimality of size-width tradeoffs for resolution
• Space bounds for resolution
• Short resolution proofs for a sequence of tricky formulas
• A combinatorial characterization of resolution width
• Space Complexity in Propositional Calculus
• Hard examples for resolution
• Short proofs are narrow—resolution made simple
• Space complexity of random formulae in resolution
• Narrow Proofs May Be Spacious:Separating Space and Width in Resolution

This page was built for publication: A simplified way of proving trade-off results for resolution