Space in Resolution
In this chapter we investigate the space complexity of resolution in particular from the point of view of the total space measure, see Sect. 3.3.We briefly review results about the clause space (Sect. 3.2) and the variable space measures (Sect. 3.4). We prove a general inequality between the total space measure and width, Theorem 3.6. Then, when talking about space it is natural to introduce a semantic version of resolution, see Sect. 3.1. We show the separation of resolution and semantic resolution and also a technique to prove total space lower bounds in semantic resolution, Theorem 3.7, and a bounded version of it, Theorem 3.8.
Unable to display preview. Download preview PDF.