On the decision problem for two-variable first-order logic
| Author(s) : | Moshe Y. Vardi Phokion G. Kolaitis Erich Gradel, |
| Publisher : | N/A |
| Publication Date : | 1997 |
| ISSN : | N/A |
| Abstract : | We identify the computational complexity of the satisfiability problem for FO 2, 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 FO, |