Space Bounds for Resolution

We introduce a new way to measure the space needed in a resolution refutation of a CNF formula in propositional logic. With the former definition [6] the space required for the resolution of any unsatisfiable formula in CNF is linear in the number of clauses. The new definition allows a much finer analysis of the space in the refutation, ranging from constant to linear space. Moreover, the new definition allows to relate the space needed in a resolution proof of a formula to other well studied complexity measures. It coincides with the complexity of a pebble game in the resolution graphs of a formula, and as we show, has strong relationships to the size of the refutation. We also give upper and lower bounds on the space needed for the resolution of unsatisfiable formulas.