We study the Guarded Fragment with Regular Guards RGF which combines the expressive power of the Guarded Fragment (GF) with Propositional Dynamic Logic with Intersection and Converse (ICPDL). Our logic generalizes, in a uniform way, many previously-studied extensions of GF, including (conjunctions of) transitive or equivalence guards, transitive or equivalence closure and more. We prove 2ExpTime-completeness of the satisfiability problem for RGF, showing that RGF is not harder than ICPDL or GF. Shifting to the query entailment problem, we provide undecidability results that significantly strengthen and solidify earlier results along those lines. We conclude by identifying the maximal, in some natural sense, ExpSpace-complete fragment of RGF.

We study Two-Variable First-Order Logic, FO2, under semantic constraints that model hierarchically structured data. Our first logic extends FO2 with a linear order < and a chain of increasingly coarser equivalence relations E_1 ⊆ E_2 ⊆ ... . We show that its finite satisfiability problem is NExpTime-complete. We also demonstrate that a weaker variant of this logic without the linear order enjoys the exponential model property. Our second logic extends FO2 with a chain of nested total preorders ⪯_1 ⊆⪯_2 ⊆ ... . We prove that its finite satisfiability problem is also NExpTime-complete.However, we show that the complexity increases to ExpSpace-complete once access to the successor relations of the preorders is allowed. Our last result is the undecidability of FO2 with two independent chains of nested equivalence relations.

The uniform one-dimensional fragment of first-order logic was introduced a few years ago as a generalization of the two-variable fragment to contexts involving relations of arity greater than two. Quantifiers in this logic are used in blocks, each block consisting only of existential quantifiers or only of universal quantifiers. In this paper we consider the possibility of mixing both types of quantifiers in blocks. We show the finite (exponential) model property and NExpTime-completeness of the satisfiability problem for two restrictions of the resulting formalism: in the first we require that every block of quantifiers is either purely universal or ends with the existential quantifier, in the second we restrict the number of variables to three; in both equality is not allowed. We also extend the second variation to a rich subfragment of the three-variable fragment (without equality) that still has the finite model property and decidable, NExpTime-complete satisfiability. Comment: arXiv admin note: text overlap with arXiv:2310.00994

Maslov's class K is an expressive fragment of First-Order Logic known to have decidable satisfiability problem, whose exact complexity, however, has not been established so far. We show that K has the exponential-sized model property, and hence its satisfiability problem is NExpTime-complete. Additionally, we get new complexity results on related fragments studied in the literature, and propose a new decidable extension of the uniform one-dimensional fragment (without equality). Our approach involves a use of satisfiability games tailored to K and a novel application of paradoxical tournament graphs.

With respect to the number of variables the border of decidability lies between 2 and 3: the two-variable fragment of first-order logic, FO2, has an exponential model property and hence NExpTime-complete satisfiability problem, while for the three-variable fragment, FO3, satisfiability is undecidable. In this paper we propose a rich subfragment of FO3, containing full FO2 (without equality), and show that it retains the finite model property and NExpTime complexity. Our fragment is obtained as an extension of the uniform one-dimensional variant of FO3.

In the last few years the field of logic-based knowledge representation took a lot of inspiration from database theory. A vital example is that the finite model semantics in description logics (DLs) is reconsidered as a desirable alternative to the classical one and that query entailment has replaced knowledge-base satisfiability (KBSat) checking as the key inference problem. However, despite the considerable effort, the overall picture concerning finite query answering in DLs is still incomplete. In this work we study the complexity of finite entailment of local queries (conjunctive queries and positive boolean combinations thereof) in the Z family of DLs, one of the most powerful KR formalisms, lying on the verge of decidability. Our main result is that the DLs ZOQ and ZOI are finitely controllable, i.e. that their finite and unrestricted entailment problems for local queries coincide. This allows us to reuse recently established upper bounds on querying these logics under the classical semantics. While we will not solve finite query entailment for the third main logic in the Z family, ZIQ, we provide a generic reduction from the finite entail- ment problem to the finite KBSat problem, working for ZIQ and some of its sublogics. Our proofs unify and solidify previously established results on finite satisfiability and finite query entailment for many known DLs.

Abstract One-dimensional fragment of first-order logic is obtained by restricting quantification to blocks of existential (universal) quantifiers that leave at most one variable free. We investigate this fragment over words and trees, presenting a complete classification of the complexity of its satisfiability problem for various navigational signatures and comparing its expressive power with other important formalisms. These include the two-variable fragment with counting and the unary negation fragment.

The Triguarded Fragment (TGF) is among the most expressive decidable fragments of first-order logic, subsuming both its two-variable and guarded fragments without equality. We show that the TGF has the finite model property (providing a tight doubly exponential bound on the model size) and hence finite satisfiability coincides with satisfiability known to be N2ExpTime-complete. Using similar constructions, we also establish 2ExpTime-completeness for finite satisfiability of the constant-free (tri)guarded fragment with transitive guards.

Abstract A complete classification of the complexity of the local and global satisfiability problems for graded modal language over traditional classes of frames has already been established. By “traditional” classes of frames, we mean those characterized by any positive combination of reflexivity, seriality, symmetry, transitivity, and the Euclidean property. In this paper, we fill the gaps remaining in an analogous classification of the graded modal language with graded converse modalities. In particular, we show its NExpTime-completeness over the class of Euclidean frames, demonstrating this way that over this class the considered language is harder than the language without graded modalities or without converse modalities. We also consider its variation disallowing graded converse modalities, but still admitting basic converse modalities. Our most important result for this variation is confirming an earlier conjecture that it is decidable over transitive frames. This contrasts with the undecidability of the language with graded converse modalities.

The triguarded fragment of first-order logic is an extension of the guarded fragment in which quantification for subformulas with at most two free variables need not be guarded. Thus, it unifies two prominent decidable logics: the guarded fragment and the two-variable fragment. Its satisfiability problem is known to be undecidable in the presence of equality, but becomes decidable when equality is forbidden. We consider an extension of the tri- guarded fragment without equality by transitive relations, allowing them to be used only as guards. We show that the satisfiability problem for the obtained formalism is decidable and 2-ExpTime-complete, that is, it is of the same complexity as for the analogous exten- sion of the classical guarded fragment. In fact, in our satisfiability test we use a decision procedure for the latter as a subroutine. We also show how our approach, consisting in exploiting some existing results on guarded logics, can be used to reprove some known facts, as well as to derive some other new results on triguarded logics.

We show that the finite satisfiability problem for the unary negation fragment with arbitrary number of transitive relations is decidable and 2-ExpTime-complete. Our result actually holds for a more general setting in which one can require that some binary symbols are interpreted as arbitrary transitive relations, some as partial orders and some as equivalences. We also consider finite satisfiability of various extensions of our primary logic, in particular capturing the concepts of nominals and role hierarchies known from description logic. As the unary negation fragment can express unions of conjunctive queries our results have interesting implications for the problem of finite query answering, both in the classical scenario and in the description logics setting.

We call a first-order formula one-dimensional if its every maximal block of existential (universal) quantifiers leaves at most one variable free. We consider the one-dimensional restrictions of the guarded fragment, GF, and the tri-guarded fragment, TGF, the latter being a recent extension of GF in which quantification for subformulas with at most two free variables need not be guarded, and which thus may be seen as a unification of GF and the two-variable fragment, FO2. We denote the resulting formalisms, resp., GF1, and TGF1. We show that GF1 has an exponential model property and NExpTime-complete satisfiability problem (that is, it is easier than full GF). For TGF1 we show that it is decidable, has the finite model property, and its satisfiability problem is TwoExpTime-complete (NExpTime-complete in the absence of equality). All the above-mentioned results are obtained for signatures with no constants. We finally discuss the impact of their addition, observing that constants do not spoil the decidability but increase the complexity of the satisfiability problem.

We consider an extension of the unary negation fragment of first-order logic in which arbitrarily many binary symbols may be required to be interpreted as equivalence relations. We show that this extension has the finite model property. More specifically, we show that every satisfiable formula has a model of at most doubly exponential size. We argue that the satisfiability (= finite satisfiability) problem for this logic is 2-ExpTime-complete. We also transfer our results to a restricted variant of the guarded negation fragment with equivalence relations.

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.

The finite satisfiability problem for the two-variable fragment of first-order logic interpreted over trees was recently shown to be ExpSpace-complete. We consider two extensions of this logic. We show that adding either additional binary symbols or counting quantifiers to the logic does not affect the complexity of the finite satisfiability problem. However, combining the two extensions and adding both binary symbols and counting quantifiers leads to an explosion of this complexity. We also compare the expressive power of the two-variable fragment over trees with its extension with counting quantifiers. It turns out that the two logics are equally expressive, although counting quantifiers do add expressive power in the restricted case of unordered trees.

A one-dimensional fragment of first-order logic is obtained by restricting quantification to blocks of existential quantifiers that leave at most one variable free. This fragment contains two-variable logic, and it is known that over words both formalisms have the same complexity and expressive power. Here we investigate the one-dimensional fragment over trees. We consider unranked unordered trees accessible by one or both of the descendant and child relations, as well as ordered trees equipped additionally with sibling relations. We show that over unordered trees the satisfiability problem is ExpSpace-complete when only the descendant relation is available and 2ExpTime-complete with both the descendant and child or with only the child relation. Over ordered trees the problem remains 2ExpTime-complete. Regarding expressivity, we show that over ordered trees and over unordered trees accessible by both the descendant and child the one-dimensional fragment is equivalent to the two-variable fragment with counting quantifiers.

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.

One-dimensional fragment of first-order logic is obtained by restricting quantification to blocks of existential quantifiers that leave at most one variable free. We investigate one-dimensional fragment over words and over omega-words. We show that it is expressively equivalent to the two-variable fragment of first-order logic. We also show that its satisfiability problem is NExpTime-complete. Further, we show undecidability of some extensions, whose two-variable counterparts remain decidable.

Verification of properties expressed in the two-variable fragment of first-order logic FO 2 has been investigated in a number of contexts. The satisfiability problem for FO 2 over arbitrary structures is known to be NEXPTIME-complete, with satisfiable formulas having exponential-sized models. Over words, where FO 2 is known to have the same expressiveness as unary temporal logic, satisfiability is again NEXPTIME-complete. Over finite labelled ordered trees, FO 2 has the same expressiveness as navigational XPath, a popular query language for XML documents. Prior work on XPath and FO 2 gives a 2EXPTIME bound for satisfiability of FO 2 over trees. This work contains a comprehensive analysis of the complexity of FO 2 on trees, and on the size and depth of models. We show that different techniques are required depending on the vocabulary used, whether the trees are ranked or unranked, and the encoding of labels on trees. We also look at a natural restriction of FO 2 , its guarded version, GF 2 . Our results depend on an analysis of types in models of FO 2 formulas, including techniques for controlling the number of distinct subtrees, the depth, and the size of a witness to satisfiability for FO 2 sentences over finite trees.

The uniform one-dimensional fragment U1 of first-order logic was introduced recently as a natural generalization of the two-variable fragment FO2 to contexts with relation symbols of all arities. It was shown that U1 has the exponential model property and NEXPTIME-complete satisfiability problem. In this paper we investigate two restrictions of U1 that still contain FO2. We call these logics RU1 and SU1, or the restricted and strongly restricted uniform one-dimensional fragments. We introduce Ehrenfeucht-Fraisse games for the logics and prove that while SU1 and RU1 are expressively equivalent, they are strictly contained in U1. Furthermore, we consider extensions of the logics SU1, RU1 and U1 with unrestricted use of a single built-in equivalence relation E. We prove that while all the obtained systems retain the finite model property, their complexities differ. Namely, the satisfiability problem is NEXPTIME-complete for SU1(E) and 2NEXPTIME-complete for both RU1(E) and U1(E). Finally, we show undecidability of some natural extensions of SU1.

We consider the satisfiability problem for modal logic over first-order definable classes of frames. We confirm the conjecture from Hemaspaandra and Schnoor [2008] that modal logic is decidable over classes definable by universal Horn formulae. We provide a full classification of Horn formulae with respect to the complexity of the corresponding satisfiability problem. It turns out, that except for the trivial case of inconsistent formulae, local satisfiability is either NP-complete or PSpace-complete, and global satisfiability is NP-complete, PSpace-complete, or ExpTime-complete. We also show that the finite satisfiability problem for modal logic over Horn definable classes of frames is decidable. On the negative side, we show undecidability of two related problems. First, we exhibit a simple universal three-variable formula defining the class of frames over which modal logic is undecidable. Second, we consider the satisfiability problem of bimodal logic over Horn definable classes of frames, and also present a formula leading to undecidability.

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.

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.

Abstract We study first-order logic with two variables FO2 and establish a small substructure property. Similar to the small model property for FO2 we obtain an exponential size bound on embedded substructures, relative to a fixed surrounding structure that may be infinite. We apply this technique to analyse the satisfiability problem for FO2 under constraints that require several binary relations to be interpreted as equivalence relations. With a single equivalence relation, FO2 has the finite model property and is complete for non-deterministic exponential time, just as for plain FO2. With two equivalence relations, FO2 does not have the finite model property, but is shown to be decidable via a construction of regular models that admit finite descriptions even though they may necessarily be infinite. For three or more equivalence relations, FO2 is undecidable.

We consider the satisfiability problem for modal logic over classes of structures definable by universal first-order formulas with three variables. We exhibit a simple formula for which the problem is undecidable. This improves an earlier result in which nine variables were used. We also show that for classes defined by three-variable, universal Horn formulas the problem is decidable. This subsumes decidability results for many natural modal logics, including T, B, K4, S4, S5.

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.

We study first-order logic with two variables FO/sup 2/ and establish a small substructure property. Similar to the small model property for FO/sup 2/ we obtain an exponential size bound on embedded substructures, relative to a fixed surrounding structure that may be infinite. We apply this technique to analyse the satisfiability problem for FO/sup 2/ under constraints that require several binary relations to be interpreted as equivalence relations. With a single equivalence relation, FO/sup 2/ has the finite model property and is complete for non-deterministic exponential time, just as for plain FO/sup 2/. With two equivalence relations, FO/sup 2/ does not have the finite model property, but is shown to be decidable via a construction of regular models that admit finite descriptions even though they may necessarily be infinite. For three or more equivalence relations, FO/sup 2/ is undecidable.