On the decision problem for two-variable first-order logic

Bulletin of Symbolic Logic 3 (1):53-69 (1997)
  Copy   BIBTEX

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 2 has the finite-model property, which means that if an FO 2 -sentence is satisfiable, then it has a finite model. Moreover, Mortimer showed that every satisfiable FO 2 -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 FO 2 -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 FO 2 is NEXPTIME-complete

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,271

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

On the restraining power of guards.Erich Grädel - 1999 - Journal of Symbolic Logic 64 (4):1719-1742.
Two variable first-order logic over ordered domains.Martin Otto - 2001 - Journal of Symbolic Logic 66 (2):685-702.
An Event-Based Fragment of First-Order Logic over Intervals.Savas Konur - 2011 - Journal of Logic, Language and Information 20 (1):49-68.
Complexity and nicety of fluted logic.William C. Purdy - 2002 - Studia Logica 71 (2):177 - 198.
Complexity of the two-variable fragment with counting quantifiers.Ian Pratt-Hartmann - 2005 - Journal of Logic, Language and Information 14 (3):369-395.
Deciding regular grammar logics with converse through first-order logic.Stéphane Demri & Hans De Nivelle - 2005 - Journal of Logic, Language and Information 14 (3):289-329.

Analytics

Added to PP
2009-01-28

Downloads
88 (#187,764)

6 months
28 (#105,140)

Historical graph of downloads
How can I increase my downloads?