Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

A simplified way of proving trade-off results for resolution

Nordström, Jakob LU (2009) In Information Processing Letters 109(18). p.1030-1035
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.

Please use this url to cite or link to this publication:
author
publishing date
type
Contribution to journal
publication status
published
subject
keywords
Automatic theorem proving, Computational complexity, Length, Proof complexity, Resolution, Space, Trade-offs, Width
in
Information Processing Letters
volume
109
issue
18
pages
6 pages
publisher
Elsevier
external identifiers
  • scopus:69049119075
ISSN
0020-0190
DOI
10.1016/j.ipl.2009.06.006
language
English
LU publication?
no
id
697a941b-4a41-47d0-970b-934986209565
date added to LUP
2020-12-18 22:28:37
date last changed
2022-02-01 18:41:09
@article{697a941b-4a41-47d0-970b-934986209565,
  abstract     = {{<p>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.</p>}},
  author       = {{Nordström, Jakob}},
  issn         = {{0020-0190}},
  keywords     = {{Automatic theorem proving; Computational complexity; Length; Proof complexity; Resolution; Space; Trade-offs; Width}},
  language     = {{eng}},
  month        = {{08}},
  number       = {{18}},
  pages        = {{1030--1035}},
  publisher    = {{Elsevier}},
  series       = {{Information Processing Letters}},
  title        = {{A simplified way of proving trade-off results for resolution}},
  url          = {{http://dx.doi.org/10.1016/j.ipl.2009.06.006}},
  doi          = {{10.1016/j.ipl.2009.06.006}},
  volume       = {{109}},
  year         = {{2009}},
}