Searching for attractive fragments of rst-order logic is an important theme in theoretical computer science. Many seminal fragments of this kind, like the two-variable fragment, FO2, [11] and the guarded fragment, GF, [2], embed, via the so-called standard translation, some modal and description logics. A more recent proposal in this vein is the unary negation fragment, UNFO, restricting the use of negation to subformulas with at most one free variable [4]. UNFO is de ned by the following grammar: ' = Bx j x = y j ' ^ ' j ' _ ' j 9x' j :'(x), where, in the rst clause, B represents any relational symbol, and, in the last clause, ' has no free variables besides (at most) x. UNFO may be seen as a generalization of basic modal and description logics to contexts with relations of arbitrary arity, alternative and orthogonal in expressive power to GF. As GF, UNFO has many good algorithmic and model theoretic properties, including the nite model property, a tree-like model property and the decidability of the satis ability (= nite satis ability) problem [4]. Besides modal and description logics, UNFO embeds also, inter alia, unions of conjunctive queries and frontier-one TGDs [3], which makes it attractive for the database and knowledge representation communities. Its serious weakness is, on the other hand, that it cannot express transitivity. This weakness is shared by FO2 and GF, both of which, moreover, become undecidable when extended by transitive relations [9, 8]. UNFO is an exception here: its satis ability problem remains decidable in the presence of arbitrarily many transitive relations. This has been explicitly stated in [10], as a corollary from the decidability of UNFO with regular path expressions, and follows also from [1], where some extensions of the guarded negation fragment are considered. From both papers the 2-ExpTime-completeness of UNFO with transitivity, UNFO+S, can be inferred. The results from [10] and [1] are obtained by employing tree-like model properties of the logics and then using some automata techniques. Since tree-like unravelings of models are in nite, such approach works only for general satisability, and gives little insight into the decidability/complexity of nite satisability, which in the case of UNFO+S is evidently a di erent problem, since, e.g., the formula 8x9yT xy ^ 8x:T xx, with transitive T , is satis able but has only in nite models. Our main contribution is demonstrating the decidability of nite satis ability for UNFO+S and establishing its 2-ExpTime-completeness. UNFO, via the above-mentioned standard translation, embeds the logic ALC, as well as its extension by inverse roles (I) and role intersections (u). Thus, being able to express conjunctive queries, we can use our results to solve, for some ? Supported by Polish NSC grant No 2016/21/B/ST6/01444. For a full version see [5].
D. Danielski and E. Kieronski
description logics, DLs, the so-called ( nite) ontology mediated query
answering problem, (F)OMQA: given a conjunctive query (or a union of conjunctive
queries) and a knowledge base speci ed in a DL, check whether the query holds
in every ( nite) model of this knowledge base. While there are quite a lot of
results for OMQA, not much is known about FOMQA. In particular, for DLs
with transitive roles (S) the only positive results we are aware of are the ones
obtained recently in [
In this context it is an interesting question if our decidability result can be
extended to capture some more expressive DLs. Unfortunately, we cannot hope
for number restrictions (Q or N ) or even functional roles (F ), as ( nite)
satis ability for UNFO with functional relations is undecidable (implicit in [
To show our basic result for UNFO+S we introduce a natural notion of treelike structures and a measure associating with transitive paths of such structures their so-called ranks. Intuitively, for a transitive relation T and a T -path , the T -rank of is the number of one-directional T -edges in . Then we show that having the following forms of models is equivalent for any formula ': (f1) nite (f2) tree-like, with bounded ranks of transitive paths (f3) tree-like, with ranks of paths bounded doubly exponentially in j'j (f4) tree-like, with ranks of paths bounded doubly exponentially in j'j, and regular (with doubly exponentially many non-isomorphic subtrees) (f5) nite, of size triply exponential in j'j.
The most di cult transitions are those from (f2) to (f3) and from (f4) to (f5).
The former is obtained in an expected way, by a kind of tree-pruning; our
pruning strategy is, however, rather intricate, due to possible interactions among
di erent transitive relations. The latter is done by an inductive construction,
building some bigger and bigger substructures of the nal model, in which some
transitive relations are total. The induction goes, roughly speaking, by the
number of non-total transitive relations in the substructure. (We used a similar small
model construction to show the nite model property for UNFO with
equivalence relations [
To show that the equivalence of the (fi) holds in the case of UNFO+SOH, we start with some preprocessing on the input formula and then reuse our model transformations for UNFO+S, treating them as black boxes. We then apply additional shrinking and pseudotransitive closure operations tailored to deal, resp., with constants and the inclusions.
Finite Satis ability of Unary Negation Fragment with Transitivity