Bulletin of Symbolic Logic 3 (1):53-69 (1997)
|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|
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
|Through your library||Configure|
Similar books and articles
Stéphane Demri & Hans De Nivelle (2005). Deciding Regular Grammar Logics with Converse Through First-Order Logic. Journal of Logic, Language and Information 14 (3):289-329.
Ian Pratt-Hartmann (2005). Complexity of the Two-Variable Fragment with Counting Quantifiers. Journal of Logic, Language and Information 14 (3):369-395.
Marcin Mostowski & Jakub Szymanik (2007). Computational Complexity of Some Ramsey Quantifiers in Finite Models. The Bulletin of Symbolic Logic 13:281--282.
Ian Pratt-Hartmann (2008). On the Computational Complexity of the Numerically Definite Syllogistic and Related Logics. Bulletin of Symbolic Logic 14 (1):1-28.
William C. Purdy (2002). Complexity and Nicety of Fluted Logic. Studia Logica 71 (2):177 - 198.
Savas Konur (2011). An Event-Based Fragment of First-Order Logic Over Intervals. Journal of Logic, Language and Information 20 (1):49-68.
Martin Otto (2001). Two Variable First-Order Logic Over Ordered Domains. Journal of Symbolic Logic 66 (2):685-702.
Erich Grädel (1999). On the Restraining Power of Guards. Journal of Symbolic Logic 64 (4):1719-1742.
Yuri Gurevich & Saharon Shelah (1983). Random Models and the Gödel Case of the Decision Problem. Journal of Symbolic Logic 48 (4):1120-1124.
Sorry, there are not enough data points to plot this chart.
Added to index2009-01-28
Total downloads1 ( #291,386 of 722,813 )
Recent downloads (6 months)1 ( #60,541 of 722,813 )
How can I increase my downloads?