Logic in Computer Science (LICS 1997)

Paper: Complexity of Two-Variable Logic with Counting (at LICS 1997)

Authors: Leszek Pacholski Wieslaw Szwast Lidia Tendera

Abstract

In the paper we consider the class C of first order sentences with two variables and with additional ``counting'' quantifiers ``there exists exactly m'' (at most, at least m), for some nonnegative integer m. We prove that the problem of satisfiability of sentences of the class with the quantifier ``there exists exactly one'' is NEXPTIME-complete. This strengthens a recent results of E. Gradel, Ph. Kolaitis and M. Vardi who proved that the satisfiability problem for the first order two-variable logic is NEXPTIME-complete and of E. Gradel, M. Otto and E. Rosen who proved the decidability of the class C. Our result easily implies that the satisfiability problem for C is in non-deterministic, doubly exponential time. It is interesting that the class C with the quantifier ``there exists exactly one'' is in NEXPTIME in spite of the fact, that there are sentences whose minimal (and only) models are of doubly exponential size.

BibTeX

  @InProceedings{PacholskiSzwastTend-ComplexityofTwoVari,
    author = 	 {Leszek Pacholski and Wieslaw Szwast and Lidia Tendera},
    title = 	 {Complexity of Two-Variable Logic with Counting},
    booktitle =  {Proceedings of the Twelfth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1997},
    year =	 1997,
    editor =	 {Glynn Winskel},
    month =	 {June}, 
    pages =      {318--327},
    location =   {Warsaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }