Complexity of the Two-Variable Fragment with (Binary-Coded) Counting Quantifiers
Ian E. Pratt-Hartmann · arXiv (Cornell University) · 2004
We show that the satisfiability and finite satisfiability problems for the two-variable fragment of first-order logic with counting quantifiers are both in NEXPTIME, even when counting quantifiers are coded succinctly.