Article

Free access

Space complexity in propositional calculus

Authors:

Michael Alekhnovich,

Eli Ben-Sasson,

Alexander A.,

Avi WigdersonAuthors Info & Claims

STOC '00: Proceedings of the thirty-second annual ACM symposium on Theory of computing

Pages 358 - 367

https://doi.org/10.1145/335305.335347

Published: 01 May 2000 Publication History

PDF eReader

References

[1]

P. Beame and T. Pitassi. Propositional proof complexity: Past, present and future. Technical report TR98- 067, Electronic Colloquium on Computational Complexity, 1998.]]

Google Scholar

[2]

E. Ben-Sasson and A. Wigderson. Short proofs axe narrow- resolution made simple. In Proceedings of the 31st ACM STOC, pages 517-526, 1999.]]

Digital Library

Google Scholar

[3]

M. Bonet and N. Galesi. A study of proof search algorithms for resolution and polynomial calculus. Manuscript, 1999.]]

Google Scholar

[4]

S. A. Cook and R. Reckhow. The relative efficiency of propositional proof systems. J. of Symbolic Logic, 44:36-50, 1979.]]

Crossref

Google Scholar

[5]

J. L. Esteban and J. Torah. Space bounds for resolution. In Proceedings of the 16th STA CS, pages 530-539, 1999.]]

Crossref

Google Scholar

[6]

G.Stalmark. Short resolution proofs for a sequence of tricky formulas. Acta Informatica, 33:277-280, 1996.]]

Digital Library

Google Scholar

[7]

S. Jukna. Exponential lower bounds for semantic resolution, in P. Beame and S. Buss, editors, Proof Complexity and Feasible Arithmetics: DIMACS workshop, April 21-2~, 1996, volume 39 of DIMACS Series in Dicrete Mathematics and Theoretical Computer Science, pages 163-172. American Math. Soc., 1997.]]

Crossref

Google Scholar

[8]

D. Kozen. Lower bounds for natural proof systems. In Proceedings of the 18th IEEE FOCS, pages 254-266, 1977.]]

Digital Library

Google Scholar

[9]

J. Krajffcek. Bounded arithmetic, propositional logic and complexity theory. Cambridge University Press, 1995.]]

Digital Library

Google Scholar

[10]

J. Krajf~ek. Interpolation theorems, lower bounds for proof systems and independence results for bounded arithmetic. Journal of Symbolic Logic, 62(2):457-486, 1997.]]

Crossref

Google Scholar

[11]

B. Krishnamurthy. Short proofs for tricky formulas. Acta Informatica, 1985.]]

Digital Library

Google Scholar

[12]

A. Razborov, A. Wigderson, and A. Yao. Read-once branching programs, rectangular proofs of the pigeonhole principle and the transversal calculus. In Proceedings of the 29th A CM Symposium on Theory of Computing, pages 739-748, 1997.]]

Digital Library

Google Scholar

[13]

J. Toran. Lower bounds for space in resolution. In CSL99, 1999.]]

Digital Library

Google Scholar

Cited By

View all

Esteban JTorán J(2019)Space bounds for resolutionInformation and Computation10.1006/inco.2001.2921171:1(84-97)Online publication date: 4-Jan-2019
https://dl.acm.org/doi/10.1006/inco.2001.2921
Ben-Sasson EGalesi N(2018)Space complexity of random formulae in resolutionRandom Structures & Algorithms10.1002/rsa.1008923:1(92-109)Online publication date: 28-Dec-2018
https://dl.acm.org/doi/10.1002/rsa.10089
Zito M(2003)An Upper Bound on the Space Complexity of Random Formulae in ResolutionRAIRO - Theoretical Informatics and Applications10.1051/ita:200300336:4(329-339)Online publication date: 15-Feb-2003
https://doi.org/10.1051/ita:2003003
Show More Cited By

Index Terms

Space complexity in propositional calculus
1. Mathematics of computing
2. Theory of computation
  1. Computational complexity and cryptography
    1. Interactive proof systems
    2. Proof complexity
  2. Logic
    1. Proof theory

Recommendations

The Lambek Calculus Extended with Intuitionistic Propositional Logic

We present sound and complete semantics and a sequent calculus for the Lambek calculus extended with intuitionistic propositional logic.
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. ...
A Cut-Free Gentzen Formulation of Basic Propositional Calculus

We introduce a Gentzen style formulation of Basic Propositional Calculus (BPC), the logic that is interpreted in Kripke models similarly to intuitionistic logic except that the accessibility relation of each model is not necessarily reflexive. The ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

STOC '00: Proceedings of the thirty-second annual ACM symposium on Theory of computing

May 2000

756 pages

ISBN:1581131844

DOI:10.1145/335305

Chairmen:
Frances Yao,
Eugene Luks

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 May 2000

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

STOC00

Sponsor:

SIGACT

STOC00: The 32nd Annual ACM Symposium on Theory of Computing

May 21 - 23, 2000

Oregon, Portland, USA

Acceptance Rates

STOC '00 Paper Acceptance Rate 85 of 182 submissions, 47%;

Overall Acceptance Rate 1,469 of 4,586 submissions, 32%

Upcoming Conference

STOC '25

Sponsor:
sigact

57th Annual ACM Symposium on Theory of Computing (STOC 2025)

June 23 - 27, 2025

Prague , Czech Republic

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
483
Total Downloads

Downloads (Last 12 months)79
Downloads (Last 6 weeks)10

Reflects downloads up to 09 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Esteban JTorán J(2019)Space bounds for resolutionInformation and Computation10.1006/inco.2001.2921171:1(84-97)Online publication date: 4-Jan-2019
https://dl.acm.org/doi/10.1006/inco.2001.2921
Ben-Sasson EGalesi N(2018)Space complexity of random formulae in resolutionRandom Structures & Algorithms10.1002/rsa.1008923:1(92-109)Online publication date: 28-Dec-2018
https://dl.acm.org/doi/10.1002/rsa.10089
Zito M(2003)An Upper Bound on the Space Complexity of Random Formulae in ResolutionRAIRO - Theoretical Informatics and Applications10.1051/ita:200300336:4(329-339)Online publication date: 15-Feb-2003
https://doi.org/10.1051/ita:2003003
Torán J(2003)Lower Bounds for Space in ResolutionComputer Science Logic10.1007/3-540-48168-0_26(362-373)Online publication date: 13-May-2003
https://doi.org/10.1007/3-540-48168-0_26
Ben-Sasson EReif J(2002)Size space tradeoffs for resolutionProceedings of the thiry-fourth annual ACM symposium on Theory of computing10.1145/509907.509975(457-464)Online publication date: 19-May-2002
https://dl.acm.org/doi/10.1145/509907.509975
Esteban JGalesi NMessner J(2002)On the Complexity of Resolution with Bounded ConjunctionsAutomata, Languages and Programming10.1007/3-540-45465-9_20(220-231)Online publication date: 25-Jun-2002
https://doi.org/10.1007/3-540-45465-9_20
Alekhnovich MRazborov A(2001)Lower bounds for polynomial calculus: non-binomial caseProceedings 42nd IEEE Symposium on Foundations of Computer Science10.1109/SFCS.2001.959893(190-199)Online publication date: 2001
https://doi.org/10.1109/SFCS.2001.959893
Alekhnovich MBen-Sasson ERazborov AWigderson A(2000)Pseudorandom generators in propositional proof complexityProceedings 41st Annual Symposium on Foundations of Computer Science10.1109/SFCS.2000.892064(43-53)Online publication date: 2000
https://doi.org/10.1109/SFCS.2000.892064
Ben-Sasson EGalesi N(2000)Space complexity of random formulae in resolutionProceedings 16th Annual IEEE Conference on Computational Complexity10.1109/CCC.2001.933871(42-51)Online publication date: 2000
https://doi.org/10.1109/CCC.2001.933871

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

The Lambek Calculus Extended with Intuitionistic Propositional Logic

Space Complexity in Propositional Calculus

A Cut-Free Gentzen Formulation of Basic Propositional Calculus