@article{GraedelKolaitisVardi:BSL:1997,
    Abstract = {We identify the computational complexity of the satisfiability problem for FO2, the fragment of first-order logic consisting of all relational first-order sentences with at most two distinct variables. Although this fragment was shown to be decidable a long time ago, the computational complexity of its decision problem has not been pinpointed so far. In 1975 Mortimer proved that FO2 has the finite-model property, which means that if an FO2-sentence is satisfiable, then it has a finite model. Moreover, Mortimer showed that every satisfiable FO2-sentence has a model whose size is at most doubly exponential in the size of the sentence. In this paper, we improve Mortimer's bound by one exponential and show that every satisfiable FO2-sentence has a model whose size is at most exponential in the size of the sentence. As a consequence, we establish that the satisfiability problem for FO2 is NEXPTIME-complete.},
    Author = {Gr{\"a}del, Erich and Kolaitis, Phokion G. and Vardi, Moshe Y.},
    File = {On the Decision Problem for Two-Variable First-Order Logic - 10.2307@421196 (0) - a - a - n.pdf},
    ISSN = {10798986},
    Journal = {The Bulletin of Symbolic Logic},
    Number = {1},
    Pages = {53--69},
    Publisher = {[Association for Symbolic Logic, Cambridge University Press]},
    Title = {On the Decision Problem for Two-Variable First-Order Logic},
    URL = {http://www.jstor.org/stable/421196},
    Volume = {3},
    Year = {1997},
    bdsk-url-1 = {http://www.jstor.org/stable/421196},
    date-added = {2019-08-20 10:46:22 +0200},
    date-modified = {2019-08-20 10:46:22 +0200},
    doi = {10.2307/421196}
}

@article{GraedelKolaitisVardi:BSL:1997, Abstract = {We identify the computational complexity of the satisfiability problem for FO2, the fragment of first-order logic consisting of all relational first-order sentences with at most two distinct variables. Although this fragment was shown to be decidable a long time ago, the computational complexity of its decision problem has not been pinpointed so far. In 1975 Mortimer proved that FO2 has the finite-model property, which means that if an FO2-sentence is satisfiable, then it has a finite model. Moreover, Mortimer showed that every satisfiable FO2-sentence has a model whose size is at most doubly exponential in the size of the sentence. In this paper, we improve Mortimer's bound by one exponential and show that every satisfiable FO2-sentence has a model whose size is at most exponential in the size of the sentence. As a consequence, we establish that the satisfiability problem for FO2 is NEXPTIME-complete.}, Author = {Gr{\"a}del, Erich and Kolaitis, Phokion G. and Vardi, Moshe Y.}, File = {On the Decision Problem for Two-Variable First-Order Logic - 10.2307@421196 (0) - a - a - n.pdf}, ISSN = {10798986}, Journal = {The Bulletin of Symbolic Logic}, Number = {1}, Pages = {53--69}, Publisher = {[Association for Symbolic Logic, Cambridge University Press]}, Title = {On the Decision Problem for Two-Variable First-Order Logic}, URL = {http://www.jstor.org/stable/421196}, Volume = {3}, Year = {1997}, bdsk-url-1 = {http://www.jstor.org/stable/421196}, date-added = {2019-08-20 10:46:22 +0200}, date-modified = {2019-08-20 10:46:22 +0200}, doi = {10.2307/421196} }