2004/01/01 by Simon Cook, Antonina Kolokolova · 1 citation
Computer Science · Mathematics · #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Advanced Algebra and Logic #Mathematics #Nondeterministic algorithm #Order (exchange) #Discrete mathematics #Horn clause #Bounded function #Set theory #Quantifier (linguistics) #Polynomial #Set (abstract data type) #Combinatorics #Algebra over a field #Pure mathematics #Computer science #Artificial intelligence
paper · doi:10.1109/lics.2004.1319634
openalex publication_date 2004/01/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/29
We introduce a second-order theory V-Krom of bounded arithmetic for nondeterministic log space. This system is based on Gradel's characterization of NL by second-order Krom formulae with only universal first-order quantifiers, which in 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 Vi-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/sub 1/-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-Szelepcsenyi theorem that NL is closed under complementation. This formalization is necessary to show that the NL functions are /spl Sigma//sub 1//sup B/-definable in V-Krom. The only other theory for NL in the literature relies on the Immerman-Szelepcsenyi's result rather than proving it.