Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR99-040 | 20th October 1999 00:00

Space Complexity in Propositional Calculus



We study space complexity in the framework of
propositional proofs. We consider a natural model analogous to
Turing machines with a read-only input tape, and such
popular propositional proof systems as Resolution, Polynomial
Calculus and Frege systems. We propose two different space measures,
corresponding to the maximal number of bits, and clauses/monomials that
need be kept in the memory simultaneously. We prove a number of lower
and upper bounds in these models, as well as some structural
results concerning the clause space for Resolution and Frege Systems.

ISSN 1433-8092 | Imprint