Logic in Computer Science (LICS 2004)

Paper: A Second-Order Theory for NL (at LICS 2004)

Authors: Stephen Cook Antonina Kolokolova

Abstract

We introduce a second-order theory V-Krom of bounded arithmetic for nondeterministic log space. This system is based on Grädel's characterization of NL by second-order Krom formulate with only universal first-order quantifiers, which is turn is motivated by the result that the decision problem for 2-CNF satisfiability is complete for coNL (and hence for NL). This theory has the style of the authors' theory V₁-Horn [APAL 124 (2003)] for polynomial time. Both theories use Zambella's elegant second-order syntax, and are axiomatized by a set 2-BASIC of simple formulae, together with a comprehension scheme for either second-order Horn formulae (in the case of V₁-Horn), or second-order Krom (2CNF) formulae (in the case of V-Krom). Our main result for V-Krom is a formalization of the Immerman-Szelepcsényi theorem that NL is closed under complementation. This formalization is necessary to show that the NL functions are \sum _1^B-definable in V-Krom. The only other theory for NL in the literature relies on the Immerman-Szelepcsényi's result rather than proving it.

BibTeX

  @InProceedings{CookKolokolova-ASecondOrderTheoryf,
    author = 	 {Stephen Cook and Antonina Kolokolova},
    title = 	 {A Second-Order Theory for NL},
    booktitle =  {Proceedings of the Nineteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2004},
    year =	 2004,
    editor =	 {Harald Ganzinger},
    month =	 {July}, 
    pages =      {398--407},
    location =   {Turku, Finland}, 
    publisher =	 {IEEE Computer Society Press}
  }