A simplified way of proving trade-off results for resolution
Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt
Standard
A simplified way of proving trade-off results for resolution. / Nordström, Jakob.
I: Information Processing Letters, Bind 109, Nr. 18, 31.08.2009, s. 1030-1035.Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - JOUR
T1 - A simplified way of proving trade-off results for resolution
AU - Nordström, Jakob
PY - 2009/8/31
Y1 - 2009/8/31
N2 - 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.
AB - 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.
KW - Automatic theorem proving
KW - Computational complexity
KW - Length
KW - Proof complexity
KW - Resolution
KW - Space
KW - Trade-offs
KW - Width
UR - http://www.scopus.com/inward/record.url?scp=69049119075&partnerID=8YFLogxK
U2 - 10.1016/j.ipl.2009.06.006
DO - 10.1016/j.ipl.2009.06.006
M3 - Journal article
AN - SCOPUS:69049119075
VL - 109
SP - 1030
EP - 1035
JO - Information Processing Letters
JF - Information Processing Letters
SN - 0020-0190
IS - 18
ER -
ID: 251870985