A Propositional Proof System for Log Space

  • Steven Perron
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3634)


The proof system G \(_{\rm 0}^{\rm *}\) of the quantified propositional calculus corresponds to NC 1, and G \(_{\rm 1}^{\rm *}\) corresponds to P, but no formula-based proof system that corresponds log space reasoning has ever been developed. This paper does this by developing GL *.

We begin by defining a class ΣCNF(2) of quantified formulas that can be evaluated in log space. Then GL * is defined as G \(_{\rm 1}^{\rm *}\) with cuts restricted to ΣCNF(2) formulas and no cut formula that is not quantifier free contains a non-parameter free variable.

To show that GL * is strong enough to capture log space reasoning, we translate theorems of Σ\(_{\rm 0}^{B}\)-rec into a family of tautologies that have polynomial size GL * proofs. Σ\(_{\rm 0}^{B}\)-rec is a theory of bounded arithmetic that is known to correspond to log space. To do the translation, we find an appropriate axiomatization of Σ\(_{\rm 0}^{B}\)-rec, and put Σ\(_{\rm 0}^{B}\)-rec proofs into a new normal form.

To show that GL * is not too strong, we prove the soundness of GL * in such a way that it can be formalized in Σ\(_{\rm 0}^{B}\)-rec. This is done by giving a log space algorithm that witnesses GL * proofs.


Normal Form Free Variable Propositional Calculus Proof System Propositional Formula 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Cook, S.: Theories for complexity classes and their propositional translations. In: Krajicek, J. (ed.) Complexity of computations and proofs. Quaderni di Matematica, pp. 175–227 (2003), Also available at
  2. 2.
    Krajicek, J., Pudlak, P.: Quantified propositional calculi and fragments of bounded arithmetic. Zeitschrift f. Mathematikal Logik u. Grundlagen d. Mathematik 36, 29–46 (1990)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Cook, S.: A survey of complexity classes and their associated propositional proof systems and theories, and a proof system for log space (2001), Available at
  4. 4.
    Pollett, C.: A propositional proof system for Ri2. In: Beame, P.W., Buss, S.R. (eds.) Proof Complexity and Feasible Arithmetics. DIMACS: Series in Discrete Mathematics and Theoretical Computer Science, vol. 39, pp. 253–278. AMS, Providence (1997)Google Scholar
  5. 5.
    Buss, S.R.: Introduction to proof theory. In: Buss, S.R. (ed.) Handbook of Proof Theory, pp. 1–78. Elsevier Science Publishers, Amsterdam (1998)CrossRefGoogle Scholar
  6. 6.
    Cook, S.: CSC 2429s: Proof complexity and bounded arithmetic. Course notes (2002), Available at
  7. 7.
    Cook, S., Morioka, T.: Quantified propositional calculus and a second-order theory for NC1 (accepted for Archive for Math. Logic)Google Scholar
  8. 8.
    Krajicek, J.: Bounded Arithmetic, Propositional Logic, and Complexity Theory. Cambridge University Press, Cambridge (1995)zbMATHCrossRefGoogle Scholar
  9. 9.
    Perron, S.: GL∗: A propositional proof system for logspace. Master’s thesis, University Of Toronto (2005), Available at
  10. 10.
    Johannsen, J.: Satisfiability problem complete for deterministic logarithmic space. In: Diekert, V., Habib, M. (eds.) STACS 2004. LNCS, vol. 2996, pp. 317–325. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  11. 11.
    Cook, S.A.: Feasibly constructive proofs and the propositional calculus. In: Proceedings of the 7-th ACM Symposium on the Theory of computation, pp. 83–97 (1975)Google Scholar
  12. 12.
    Zambella, D.: End extensions of models of linearly bounded arithmetic. Annals of Pure and Applied Logic 88, 263–277 (1997)zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    Cook, S.A., McKenzie, P.: Problems complete for deterministic logarithmic space. Journal of Algorithms 8, 385–394 (1987)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Steven Perron
    • 1
  1. 1.Department of Computer ScienceUniversity of Toronto 

Personalised recommendations