A simplified way of proving trade-off results for resolution

DOI10.1016/J.IPL.2009.06.006MaRDI QIDQ989569zbMATH OpenOpenAlexFDO

Authors Jakob Nordstrom

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 complexityresolutionlengthproof complexityautomatic theorem provingwidthspacetrade-offs

Mathematics Subject Classification ID

Recommendations

• Size-space tradeoffs for resolution
• A tradeoff between length and width in resolution
• Time-space trade-offs in resolution: superpolynomial lower bounds for superlinear space
• On space and depth in resolution
• Supercritical space-width trade-offs for resolution

Cites work

• scientific article; zbMATH DE number 3888913 (Why is no real title available?)
• scientific article; zbMATH DE number 1424047 (Why is no real title available?)
• scientific article; zbMATH DE number 5485584 (Why is no real title available?)
• A combinatorial characterization of resolution width
• Hard examples for resolution
• Narrow proofs may be spacious: separating space and width in resolution
• Optimality of size-width tradeoffs for resolution
• Short proofs are narrow—resolution made simple
• Short resolution proofs for a sequence of tricky formulas
• Space Complexity in Propositional Calculus
• Space bounds for resolution
• Space complexity of random formulae in resolution
• The complexity of facets resolved

Cited in

(8)

• A tradeoff between length and width in resolution
• Time-space trade-offs in resolution: superpolynomial lower bounds for superlinear space
• An Introduction to Lower Bounds on Resolution Proof Systems
• Nullstellensatz size-degree trade-offs from reversible pebbling
• From small space to small width in resolution
• Contradiction separation based dynamic multi-clause synergized automated deduction
• Space Complexity in Polynomial Calculus
• Strong extension-free proof systems

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

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