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)
DOI 10.2307/421196
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 55,856
Through your library

References found in this work BETA

On Computable Numbers, with an Application to the N Tscheidungsproblem.Alan Turing - 1936 - Proceedings of the London Mathematical Society 42 (1):230-265.
Some Philosophical Problems From the Standpoint of Artificial Intelligence.John McCarthy & Patrick Hayes - 1969 - In B. Meltzer & Donald Michie (eds.), Machine Intelligence 4. Edinburgh University Press. pp. 463--502.
A Note on the Entscheidungsproblem.Alonzo Church - 1936 - Journal of Symbolic Logic 1 (1):40-41.
On Languages with Two Variables.Michael Mortimer - 1975 - Mathematical Logic Quarterly 21 (1):135-140.

View all 15 references / Add more references

Citations of this work BETA

Logics for the Relational Syllogistic.Ian Pratt-Hartmann & Lawrence S. Moss - 2009 - Review of Symbolic Logic 2 (4):647-683.
On the Restraining Power of Guards.Erich Grädel - 1999 - Journal of Symbolic Logic 64 (4):1719-1742.
Lattice Logic as a Fragment of (2-Sorted) Residuated Modal Logic.Chrysafis Hartonas - 2019 - Journal of Applied Non-Classical Logics 29 (2):152-170.
Modal Translation of Substructural Logics.Chrysafis Hartonas - 2020 - Journal of Applied Non-Classical Logics 30 (1):16-49.

View all 25 citations / Add more citations

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 index
2009-01-28

Total views
44 ( #226,424 of 2,401,723 )

Recent downloads (6 months)
1 ( #551,964 of 2,401,723 )

How can I increase my downloads?

Downloads

My notes