Abstract The main motivation for this work is the open question of decidability of the satisfiability problem for the two-variable fragment of first-order logic, ${\mathcal{FO}^{2}}$, with one transitive relation. In the presence of equality, the problem can be reduced to the corresponding problem when the transitive relation is required to be a strict partial order. It is known that its finite satisfiability problem is decidable but the decidability of the general satisfiability problem has been resolved only for restricted variants. More precisely, the problem is decidable for the fragment with comparable witnesses in which existential quantifiers are required to be guarded by atoms of the form $x

The fluted fragment is a recently rediscovered decidable fragment of first-order logic whose history is dating back to Quine and the sixties of the 20th century. The fragment is defined by fixing simultaneously the order in which variables occur in atomic formulas and the order of quantification of variables; no further restrictions concerning e.g. the number of variables, guardedness or usage of negation apply. In the talk we review some motivation and the history of the fragment, discuss the differences between the fluted fragment and other decidable fragments of first-order logic, present its basic model theoretic and algorithmic properties, and discuss recent work concerning limits of decidability of its extensions.

We study the satisfiability problem for the fluted fragment extended with transitive relations. We show that the logic enjoys the finite model property when only one transitive relation is available. On the other hand we show that the satisfiability problem is undecidable already for the two-variable fragment of the logic in the presence of three transitive relations.

Abstract We study the fluted fragment, a decidable fragment of first-order logic with an unbounded number of variables, motivated by the work of W. V. Quine. We show that the satisfiability problem for this fragment has nonelementary complexity, thus refuting an earlier published claim by W. C. Purdy that it is in NExpTime. More precisely, we consider ${\cal F}{{\cal L}^m}$ , the intersection of the fluted fragment and the m-variable fragment of first-order logic, for all $m \ge 1$ . We show that, for $m \ge 2$ , this subfragment forces $\left\lfloor {m/2} \right\rfloor$ -tuply exponentially large models, and that its satisfiability problem is $\left\lfloor {m/2} \right\rfloor$ -NExpTime-hard. We further establish that, for $m \ge 3$ , any satisfiable ${\cal F}{{\cal L}^m}$ -formula has a model of at most ( $m - 2$ )-tuply exponential size, whence the satisfiability (= finite satisfiability) problem for this fragment is in ( $m - 2$ )-NExpTime. Together with other, known, complexity results, this provides tight complexity bounds for ${\cal F}{{\cal L}^m}$ for all $m \le 4$ .

Abstract We study the satisfiability problem for two-variable first-order logic over structures with one transitive relation. We show that the problem is decidable in 2-NExpTime for the fragment consisting of formulas where existential quantifiers are guarded by transitive atoms. As this fragment enjoys neither the finite model property nor the tree model property, to show decidability we introduce a novel model construction technique based on the infinite Ramsey theorem. We also point out why the technique is not sufficient to obtain decidability for the full two-variable logic with one transitive relation; hence, contrary to our previous claim, [FO$^2$ with one transitive relation is decidable, STACS 2013: 317-328], the status of the latter problem remains open.

We consider extensions of the two-variable guarded fragment, GF 2 , where distinguished binary predicates that occur only in guards are required to be interpreted in a special way (as transitive relations, equivalence relations, preorders, or partial orders). We prove that the only fragment that retains the finite (exponential) model property is GF 2 with equivalence guards without equality. For remaining fragments, we show that the size of a minimal finite model is at most doubly exponential. To obtain the result, we invent a strategy of building finite models that are formed from a number of multidimensional grids placed over a cylindrical surface. The construction yields a 2-NE xp T ime upper bound on the complexity of the finite satisfiability problem for these fragments. We improve the bounds and obtain optimal ones for all the fragments considered, in particular NE xp T ime for GF 2 with equivalence guards, and 2-E xp T ime for GF 2 with transitive guards . To obtain our results, we essentially use some results from integer programming.

We consider the satisfiability and finite satisfiability problems for the extension of the two-variable guarded fragment in which an equivalence closure operator can be applied to two distinguished binary predicates.We show that the satisfiability and finite satisfiability problems for this logic are 2-ExpTime-complete.This contrasts with an earlier result that the corresponding problems for the full two-variable logic with equivalence closures of two binary predicates are 2-NExpTime-complete.

We study the fluted fragment, a decidable fragment of first-order logic with an unbounded number of variables, originally identified by W.V. Quine. We show that the satisfiability problem for this fragment has non-elementary complexity, thus refuting an earlier published claim by W.C. Purdy that it is in NExpTime. More precisely, we consider, for all m greater than 1, the intersection of the fluted fragment and the m-variable fragment of first-order logic. We show that this sub-fragment forces (m/2)-tuply exponentially large models, and that its satisfiability problem is (m/2)-NExpTime-hard. We round off by using a corrected version of Purdy's construction to show that the m-variable fluted fragment has the m-tuply exponential model property, and that its satisfiability problem is in m-NExpTime.

We consider the satisfiability and finite satisfiability problems for extensions of the two-variable fragment of first-order logic in which an equivalence closure operator can be applied to a fixed number of binary predicates. We show that the satisfiability problem for two-variable, first-order logic with equivalence closure applied to two binary predicates is in 2-NExpTime, and we obtain a matching lower bound by showing that the satisfiability problem for two-variable first-order logic in the presence of two equivalence relations is 2-NExpTime-hard. The logics in question lack the finite model property; however, we show that the same complexity bounds hold for the corresponding finite satisfiability problems. We further show that the satisfiability (${=}$ finite satisfiability) problem for the two-variable fragment of first-order logic with equivalence closure applied to a single binary predicate is NExpTime-complete.

In this talk we survey recent work in the quest for expressive logics with good algorithmic properties, starting from the two-variable fragment of first-order logic and the guarded fragment. While tracing the boundary between decidable and undecidable fragments we describe their power, limitations, similarities and differences in order to stress out key properties responsible for their good or bad behaviour. We also highlight tools and techniques that have proven most effective for designing optimal algorithms, special attention giving to the more universal ones.

We show that the satisfiability problem for the two-variable first-order logic, FO^2, over transitive structures when only one relation is required to be transitive, is decidable. The result is optimal, as FO^2 over structures with two transitive relations, or with one transitive and one equivalence relation, are known to be undecidable, so in fact, our result completes the classification of FO^2-logics over transitive structures with respect to decidability. We show that the satisfiability problem is in 2-NExpTime. Decidability of the finite satisfiability problem remains open.

We consider the satisfiability and finite satisfiability problems for extensions of the two-variable fragment of first-order logic in which an equivalence closure operator can be applied to a fixed number of binary predicates. We show that the satisfiability problem for two-variable, first-order logic with equivalence closure applied to two binary predicates is in 2NEXPTIME, and we obtain a matching lower bound by showing that the satisfiability problem for two-variable first-order logic in the presence of two equivalence relations is 2NEXPTIME-hard. The logics in question lack the finite model property; however, we show that the same complexity bounds hold for the corresponding finite satisfiability problems. We further show that the satisfiability (=finite satisfiability) problem for the two-variable fragment of first-order logic with equivalence closure applied to a single binary predicate is NEXPTIME-complete.

We show that every finitely satisfiable two-variable first-order formula with two equivalence relations has a model of size at most triply exponential with respect to its length. Thus the finite satisfiability problem for two-variable logic over the class of structures with two equivalence relations is decidable in nondeterministic triply exponential time. We also show that replacing one of the equivalence relations in the considered class of structures by a relation which is only required to be transitive leads to undecidability. This sharpens the earlier result that two-variable logic is undecidable over the class of structures with two transitive relations.

The guarded fragment with transitive guards, [GF+TG], is an extension of GF in which certain relations are required to be transitive, transitive predicate letters appear only in guards of the quantifiers and the equality symbol may appear everywhere. We prove that the decision problem for [GF+TG] is decidable. This answers the question posed in (Ganzinger et al., 1999). Moreover, we show that the problem is 2EXPTIME-complete. This result is optimal since the satisfiability problem for GF is 2EXPTIME-complete (Gradel, 1999). We also show that the satisfiability problem for two-variable [GF+TG] is NEXPTIME-hard in contrast to GF with bounded number of variables for which the satisfiability problem is EXPTIME-complete.

Let $C^2_p$ denote the class of first-order sentences with two variables and with additional quantifiers "there exists exactly (at most, at least) i" for $i\leq p$, and let $C^2$ be the union of $C^2_p$ taken over all integers p. We prove that the satisfiability problem for $C^2_1$ sentences is NEXPTIME-complete. This strengthens the results by [E. Grädel, Ph. Kolaitis, and M. Vardi, Bull. Symbolic Logic, 3 (1997), pp. 53--69], who showed that the satisfiability problem for the first-order two-variable logic $L^2$ is NEXPTIME-complete and by [E. Grädel, M. Otto, and E. Rosen, 12th Annual IEEE Symposium on Logic in Computer Science, 1997, pp. 306--317], who proved the decidability of $C^2$. Our result easily implies that the satisfiability problem for $C^2$ is in nondeterministic, doubly exponential time. It is interesting that $C^2_1$ is in NEXPTIME in spite of the fact that there are sentences whose minimal (and only) models are of doubly exponential size. It is worth noticing that by a recent result of [E. Grädel, M. Otto, and E. Rosen, Proceedings of 14th Annual Symposium on Theoretical Aspects of Computer Science, Lecture Notes in Comput. Sci. 1200, Springer-Verlag, Berlin, 1997], extensions of two-variable logic $L^2$ by a weak access to cardinalities through the Härtig (or equicardinality) quantifier is undecidable. The same is true for extensions of $L^2$ by very weak forms of recursion. The satisfiability problem for logics with a bounded number of variables has applications in artificial intelligence, notably in modal logics (see, e.g., [W. van der Hoek and M. De Rijke, J. Logic Comput., 5 (1995), pp. 325--345]), where counting comes in the context of graded modalities and in description logics, where counting can be used to express so-called number restrictions (see, e.g., [A. Borgida, Artificial Intelligence, 82 (1996), pp. 353--367]).

Let C/sub k//sup 2/ denote the class of first order sentences with two variables and with additional quantifiers "there exists exactly (at most, at least) m", for m/spl les/k, and let C/sup 2/ be the union of C/sub k//sup 2/ taken over all integers k. We prove that the problem of satisfiability of sentences of C/sub 1//sup 2/ is NEXPTIME-complete. This strengthens a recent result of E. Gradel, Ph. Kolaitis and M. Vardi (1997) who proved that the satisfiability problem for the first order two-variable logic L/sup 2/ is NEXPTIME-complete and a very recent result by E. Gradel, M. Otto and E. Rosen (1997) who proved the decidability of C/sup 2/. Our result easily implies that the satisfiability problem for C/sup 2/ is in non-deterministic, doubly exponential time. It is interesting that C/sub 1//sup 2/ is in NEXPTIME in spite of the fact, that there are sentences whose minimal (and only) models are of doubly exponential size.

The Σ 1 1 (∀∃∀) class is the class of all existential second-order sentences whose first-order part is in the prenex form with prefix of the form ∀∃∀. In this paper we prove that every rational number in the interval [0,1] is the asymptotic probability for some Σ 1 1 (∀∃∀) sentence. This result completes the classification of asymptotic probabilities for the existential second-order minimal classes.