Treffer: Space Complexity in Propositional Calculus: Space complexity in propositional calculus
Title:
Space Complexity in Propositional Calculus: Space complexity in propositional calculus
Authors:
Source:
SIAM Journal on Computing. 31:1184-1211
Publisher Information:
Society for Industrial & Applied Mathematics (SIAM), 2000.
Publication Year:
2000
Subject Terms:
Complexity of proofs, Complexity of computation (including implicit computational complexity), resolution, 0102 computer and information sciences, 01 natural sciences, Mechanization of proofs and logical operations, Classical propositional logic, upper bounds, lower bounds, proof complexity, polynomial calculus, 0101 mathematics, space complexity, Frege systems
Document Type:
Fachzeitschrift
Article
File Description:
application/xml
Language:
English
ISSN:
1095-7111
0097-5397
0097-5397
DOI:
10.1137/s0097539700366735
DOI:
10.1145/335305.335347
Access URL:
https://epubs.siam.org/doi/abs/10.1137/S0097539700366735
https://dl.acm.org/doi/10.1137/S0097539700366735
https://dblp.uni-trier.de/db/journals/siamcomp/siamcomp31.html#AlekhnovichBRW02
https://dl.acm.org/doi/10.1145/335305.335347
https://dblp.uni-trier.de/db/conf/stoc/stoc2000.html#AlekhnovichBRW00
http://core.ac.uk/display/23812557
https://dl.acm.org/doi/10.1137/S0097539700366735
https://dblp.uni-trier.de/db/journals/siamcomp/siamcomp31.html#AlekhnovichBRW02
https://dl.acm.org/doi/10.1145/335305.335347
https://dblp.uni-trier.de/db/conf/stoc/stoc2000.html#AlekhnovichBRW00
http://core.ac.uk/display/23812557
Accession Number:
edsair.doi.dedup.....db3a1bde52ddf4461ea3eed91e4affc8
Database:
OpenAIRE
Weitere Informationen
Summary: 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 to 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.