## 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} }