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. (shrink)

Guarded fragments of first-order logic were recently introduced by Andreka, van Benthem and Nemeti; they consist of relational first-order formulae whose quantifiers are appropriately relativized by atoms. These fragments are interesting because they extend in a natural way many propositional modal logics, because they have useful model-theoretic properties and especially because they are decidable classes that avoid the usual syntactic restrictions (on the arity of relation symbols, the quantifier pattern or the number of variables) of almost all other known decidable (...) fragments of first-order logic. Here, we investigate the computational complexity of these fragments. We prove that the satisfiability problems for the guarded fragment (GF) and the loosely guarded fragment (LGF) of first-order logic are complete for deterministic double exponential time. For the subfragments that have only a bounded number of variables or only relation symbols of bounded arity, satisfiability is EXPTIME-complete. We further establish a tree model property for both the guarded fragment and the loosely guarded fragment, and give a proof of the finite model property of the guarded fragment. It is also shown that some natural, modest extensions of the guarded fragments are undecidable. (shrink)

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. (shrink)

The satisfiability and finite satisfiability problems for the two-variable fragment of first-order logic with counting quantifiers are both in NEXPTIME, even when counting quantifiers are coded succinctly.

Description Logics are a family of knowledge representation formalisms mainly characterised by constructors to build complex concepts and roles from atomic ones. Expressive role constructors are important in many applications, but can be computationally problematical.We present an algorithm that decides satisfiability of the DL ALC extended with transitive and inverse roles and functional restrictions with respect to general concept inclusion axioms and role hierarchies; early experiments indicate that this algorithm is well-suited for implementation. Additionally, we show that ALC extended with (...) just transitive and inverse roles is still in PSPACE. We investigate the limits of decidability for this family of DLs, showing that relaxing the constraints placed on the kinds of roles used in number restrictions leads to the undecidability of all inference problems. Finally, we describe a number of optimisation techniques that are crucial in obtaining implementations of the decision procedures, which, despite the high worst-case complexity of the problem, exhibit good performance with real-life problems. (shrink)

What precisely are fragments of classical first-order logic showing “modal” behaviour? Perhaps the most influential answer is that of Gabbay 1981, which identifies them with so-called “finite-variable fragments”, using only some fixed finite number of variables (free or bound). This view-point has been endorsed by many authors (cf. van Benthem 1991). We will investigate these fragments, and find that, illuminating and interesting though they are, they lack the required nice behaviour in our sense. (Several new negative results support this claim.) (...) As a counterproposal, then, we define a large fragment of predicate logic characterized by its use of only bounded quantification. This so-called guarded fragment enjoys the above nice properties, including decidability, through an effectively bounded finite model property. (These are new results, obtained by generalizing notions and techniques from modal logic.) Moreover, its own internal finite variable hierarchy turns out to work well. Finally, we shall make another move. The above analogy works both ways. Modal operators are like quantifiers, but quantifiers are also like modal operators. This observation inspires a generalized semantics for first-order predicate logic with accessibility constraints on available assignments (cf. N´emeti 1986, 1992) which moves the earlier quantifier restrictions into the semantics. This provides a fresh look at the landscape of possible predicate logics, including candidates sharing various desirable features with basic modal logic – in particular, its decidability. (shrink)

This book offers a comprehensive treatment of the classical decision problem of mathematical logic and of the role of the classical decision problem in modern computer science. The text presents a revealing analysis of the natural order of decidable and undecidable cases and includes a number of simple proofs and exercises.