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 -