Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Twelfth Annual IEEE Symposium on

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 Symposium on Logic in Computer Science (LICS 1997)},
    year =	 {1997},
    month =	 {June}, 
    pages =      {318--327},
    location =   {Warsaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski