A simplified way of proving trade-off results for resolution

Jakob Nordström

doi:10.1016/j.ipl.2009.06.006

A simplified way of proving trade-off results for resolution

Jakob Nordström

Massachusetts Institute of Technology

Forskningsoutput: Tidskriftsbidrag › Artikel i vetenskaplig tidskrift › Peer review

Sammanfattning

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.

Originalspråk	engelska
Sidor (från-till)	1030-1035
Antal sidor	6
Tidskrift	Information Processing Letters
Volym	109
Nummer	18
DOI	https://doi.org/10.1016/j.ipl.2009.06.006
Status	Published - 2009 aug. 31
Externt publicerad	Ja

Ämnesklassifikation (UKÄ)

Datavetenskap (datalogi)

Tillgång till dokument

10.1016/j.ipl.2009.06.006

Citera det här

@article{697a941b4a4147d0970b934986209565,

title = "A simplified way of proving trade-off results for resolution",

abstract = "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.",

keywords = "Automatic theorem proving, Computational complexity, Length, Proof complexity, Resolution, Space, Trade-offs, Width",

author = "Jakob Nordstr{\"o}m",

year = "2009",

month = aug,

day = "31",

doi = "10.1016/j.ipl.2009.06.006",

language = "English",

volume = "109",

pages = "1030--1035",

journal = "Information Processing Letters",

issn = "0020-0190",

publisher = "Elsevier",

number = "18",

}

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

U2 - 10.1016/j.ipl.2009.06.006

DO - 10.1016/j.ipl.2009.06.006

M3 - Article

AN - SCOPUS:69049119075

SN - 0020-0190

VL - 109

SP - 1030

EP - 1035

JO - Information Processing Letters

JF - Information Processing Letters

IS - 18

ER -

A simplified way of proving trade-off results for resolution

Sammanfattning

Ämnesklassifikation (UKÄ)

Tillgång till dokument

Fingeravtryck

Citera det här