A simplified way of proving trade-off results for resolution
2009 (English)In: Information Processing Letters, ISSN 0020-0190, E-ISSN 1872-6119, Vol. 109, no 18, 1030-1035 p.Article in journal (Refereed) Published
We present a greatly simplified proof of the length-space trade-off result for resolution in [P. Hertel, T. Pitassi, Exponential time/space speedups for resolution and the PSPACE-completeness of black-white pebbling, in: Proceedings of the 48th Annual IEEE Symposium on Foundations of Computer Science (FOCS '07), Oct. 2007, pp. 137-149], and also prove a couple of other theorems in the same vein. We point out two important ingredients needed for our proofs to work, and discuss some possible conclusions. Our key trick is to look at formulas of the type F = G ∧ H, where G and H are over disjoint sets of variables and have very different length-space properties with respect to resolution.
Place, publisher, year, edition, pages
2009. Vol. 109, no 18, 1030-1035 p.
Automatic theorem proving, Computational complexity, Length, Proof complexity, Resolution, Space, Trade-offs, Width
IdentifiersURN: urn:nbn:se:kth:diva-81072DOI: 10.1016/j.ipl.2009.06.006ISI: 000270126700003OAI: oai:DiVA.org:kth-81072DiVA: diva2:497094
QC 201202162012-02-102012-02-102012-02-16Bibliographically approved