## Paper: Two-variable logic with counting is decidable (at LICS 1997)

Authors:**Erich Graedel Martin Otto Eric Rosen**

### Abstract

We prove that the satisfiability and the finite satisfiability problems for C^2 are decidable. C^2 is first-order logic with only two variables in the presence of arbitrary counting quantifiers, "there exist at least m elements x", for m a natural number. It considerably extends L^2, plain first-order with only two variables, which is known to be decidable by a result of Mortimer's. Unlike L^2, C^2 does not have the finite model property.

### BibTeX

@InProceedings{GraedelOttoRosen-Twovariablelogicwit, author = {Erich Graedel and Martin Otto and Eric Rosen}, title = {Two-variable logic with counting is decidable}, booktitle = {Proceedings of the Twelfth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1997}, year = 1997, editor = {Glynn Winskel}, month = {June}, pages = {306--317}, location = {Warsaw, Poland}, publisher = {IEEE Computer Society Press} }