On Finite and Unrestricted Query Entailment beyond SQ with Number Restrictions on Transitive Roles

1 Introduction

A prominent line of research in knowledge representation and database theory has focused on the evaluation of queries over incomplete data enriched by ontologies providing background knowledge. In this paradigm, ontologies are commonly formulated using description logics (DLs), believed to offer a good balance between expressivity and complexity. This is supported, for instance, by the good understanding of 'data-tractable' DLs [Kontchakov and Zakharyaschev, 2014; Bienvenu and Ortiz, 2015]. Yet, for some expressive DLs the complexity of query entailment is less understood.

In this paper, we study query entailment in extensions of the description logic (DL) SQ allowing number restrictions (Q) to be applied to transitive roles (S). Most previous work on query entailment in expressive DLs, such as SHIQ or SHOQ, forbid the interaction of number restrictions and transitive roles [Glimm et al., 2008b; Glimm et al., 2008a; Calvanese et al., 2014], but it is required in areas like biomedicine, e.g., to restrict the number of certain parts an organ has. For instance, one can express that the human heart has exactly one mitral valve, which has to be shared by its left and right atrium [Guti´errez-Basulto et al., 2018]. Allowing for the interaction of S and Q is dangerous in the sense that even modest extensions of SQ, such as with role inclusions or inverse roles, lead to an undecidable satisfiability problem [Kazakov et al., 2007]. Decidability of satisfiability in SQ and in its extension with nominals was shown several years ago [Kazakov et al., 2007;

Kaminski and Smolka, 2010], but only recently tight computational complexity bounds were established [Guti´errezBasulto et al., 2017]. Even more recently, decidability for entailment of regular path queries over SQ knowledge bases was established. More precisely, based on a novel tree-like model property of SQ it was possible to devise an automatabased decision procedure yielding a tight 2EXPTIME upper bound [Guti´errez-Basulto et al., 2018].

The objective of this paper is to provide a more complete picture of query entailment in DLs with number restrictions on transitive roles. We pursue two specific goals.

First, we aim at understanding the limits of decidability of query entailment for such DLs. To this end, we investigate the extensions of SQ by nominals (SOQ) and controlled inverse roles (SIQ- ), where we allow number restrictions on inverse non-transitive roles and only existential restrictions on inverse transitive roles. As query language, we consider positive existential regular path queries, thus capturing the common languages of conjunctive and regular path queries.

Our second aim is to initiate the study of finite query entailment for SIQ- and SOQ, where one is interested in reasoning only over finite models. This distinction is crucial because in database applications, both database instances and the models they represent are commonly assumed to be finite. The study of finite query entailment in SQ is interesting since, due to the presence of transitivity, SQ lacks finite controllability, and therefore unrestricted and finite entailment do not coincide. Interestingly, most previous works on finite query entailment consider logics lacking finite controllability because of number restrictions and inverse roles [Rosati, 2008; Pratt-Hartmann, 2009; Ib´a˜nez-Garc´ıa et al., 2014; Amarilli and Benedikt, 2015]. The study of finite query entailment in logics with transitivity (without number restrictions on transitive roles) started only recently [Rudolph, 2016; Gogacz et al., 2018; Danielski and Kieronski, 2018]. Here, we focus on finite entailment of positive existential queries in SOQ and of instance queries in SIQ- .

Our main contributions are as follows. In Sect. 3, we start by showing a tree-like model property for both SOQ and SIQ- . More specifically, we carefully extend and adapt the canonical tree decompositions that were introduced for SQ in previous work [Guti´errez-Basulto et al., 2018] to also incorporate the presence of controlled inverses and nominals. Next, we prove that if a query is not entailed by a knowledge base (KB), then there is a counter-model with a canonical tree decomposition of small width. This tree-like model property is the basis for automata-based approaches to unrestricted and finite query entailment in the remainder of the paper. First, in Sect. 4, we construct tree automata to optimally decide entailment of regular path queries over SOQ and SIQ- KBs in 2EXPTIME. We move then, in Sect. 5, to finite entailment of positive existential queries over SOQ KBs, showing again an optimal 2EXPTIME upper bound. To this end, we look at more refined canonical tree decompositions, which ensure the existence of a finite counter model. In other words, we reduce finite query entailment to entailment over models with this special canonical tree decomposition. Finally, in Sect. 6, we investigate the complexity for unrestricted and finite instance query (IQ) entailment in SIQ- . In particular, we show that IQ entailment is 2EXPTIME-hard both in the finite and in the unrestricted case. We found this surprising since it is rarely the case that IQ entailment becomes more difficult when inverses are added to the logic. Moreover, the result provides an orthogonal reason for 2EXPTIME-hardness for conjunctive query entailment in SIQ- [Lutz, 2008]. We complement this lower bound with matching upper bounds in the unrestricted case, thus confirming the conjecture that satisfiability in SIQ- is decidable [Kazakov et al., 2007]. In the finite case, we show a 2EXPTIME-upper bound for KBs using a single transitive role. Note that SIQ- with a single transitive role is a notational variant of the graded modal logic with converse K4(♦≥, ♦- ). Thus, our result entails 2EXPTIMEcompleteness for global consequence in K4(♦≥, ♦- ), which was only known to be decidable [Bednarczyk et al., 2019].

A long version with appendix can be found under http:// www.informatik.uni-bremen.de/tdki/research/papers.html.

2 Preliminaries

Description Logics

We consider a vocabulary consisting of countably infinite disjoint sets of concept names NC, role names NR, and individual names NI, and assume that NR is partitioned into two infinite sets of non-transitive role names N nt R and transitive role names N t R . A role is a role name or an inverse role r-; a transitive role is a transitive role name or the inverse of one. SIQ- -concepts C, D are defined by the grammar

where A ∈ NC, r is a role, n ≥ 0 is a natural number given in binary, and s is either a non-transitive role or a transitive role name. SOQ-concepts C, D are defined by the grammar

where A ∈ NC, r ∈ NR, a ∈ NI and n is as above. We will use (⩾ n r C) as abbreviation for ¬(⩽ n-1 r C), together with standard abbreviations ⊥, ⊤, C ⊔D, ∀r.C. Concepts of the form (⩽ n r C), (⩾ n r C), and {a} are called at-most restrictions, at-least restrictions, and nominals, respectively. Note that in SIQ- concepts, inverse transitive roles are not allowed in at-most and at-least restrictions.

A SIQ- -TBox (respectively, SOQ-TBox) T is a finite set of concept inclusions (CIs) C ⊑ D, where C,D are SIQ- - concepts (respectively, SOQ-concepts). An ABox A is a finite non-empty set of concept and role assertions of the form A(a), r(a, b) where A ∈ NC, r ∈ NR and {a, b} ⊆ NI; ind(A) is the set of individual names occurring in A. A knowledge base (KB) is a pair K = (T , A); nom(K) is the set of nominals occurring in K and ind(K) = ind(A) ∪ nom(K).

Without loss of generality, we assume throughout the paper that all CIs are in one of the following normal forms:

where A,Ai,B,Bj are concept names or nominals, r ∈ NR, s is a non-transitive role or a transitive role name, and empty disjunction and conjunction are equivalent to ⊥ and ⊤, respectively. We further assume that for every at-most and atleast restriction, T contains an equivalent concept name.

Interpretations

The semantics is given as usual via interpretations I = (∆I , ·I ) consisting of a non-empty domain ∆I and an interpretation function ·I mapping concept names to subsets of the domain and role names to binary relations over the domain. Further, we adopt the standard name assumption, i.e., aI = a for all a ∈ NI. The interpretation of complex concepts C is defined in the usual way [Baader et al., 2017]. An interpretation I is a model of a TBox T , written I |= T if C I ⊆ DI for all CIs C ⊑ D ∈ T . It is a model of an ABox A, written I |= A, if (a, b) ∈ rI for all r(a, b) ∈ A and a ∈ AI for all A(a) ∈ A. Finally, I is a model of a KB K = (T ,A), written I |= K, if I |= T , I |= A, and rI is transitive for all r ∈ N t R occurring in K. If K has a model, we say that it is satisfiable.

An interpretation I ′ is a sub-interpretation of I, written as I ′ ⊆ I, if ∆I ′ ⊆ ∆I , AI ′ ⊆ AI , and rI ′ ⊆ rI for all A ∈ NC and r ∈ NR. For Σ ⊆ NC ∪ NR, I is a Σinterpretation if AI = ∅ and rI = ∅ for all A ∈ NC \ Σ and r ∈ NR \ Σ. The restriction of I to signature Σ is the maximal Σ-interpretation I ′ with I ′ ⊆ I. The restriction of I to domain ∆ is the maximal sub-interpretation of I with domain ∆. The union I ∪ J of I and J is an interpretation such that ∆I∪J = ∆I ∪∆J , AI∪J = AI ∪AJ , and rI∪J = rI ∪ rJ for all A ∈ NC and r ∈ NR. The transitive closure I ∗ of I is an interpretation such that ∆I ∗ = ∆I , AI ∗ = AI for all A ∈ NC, rI ∗ = rI for all r ∈ N nt R , and rI ∗ = (rI )+ for all r ∈ N t R .

A tree decomposition T of an interpretation I is a pair (T, I) where T is a tree and I is a function that assigns an interpretation I(w) = (∆w, ·I(w) ) to each w ∈ T such that I = ⋃w∈T I(w) and for every d ∈ ∆I , the set {w ∈ T | d ∈ ∆w} is connected in T . We often blur the distinction between a node w of T and the associated interpretation I(w), using the term bag for both. The width of T is supw∈T |∆w| - 1; the outdegree of T is the outdegree of T. For each d ∈ ∆I , there is a unique bag w closest to the root ε such that d ∈ ∆w. We say that d is fresh in this bag, and write F(w) for the set of all elements fresh in w.

Ontology-mediated Query Entailment

A positive existential regular path query (PRPQ) is a firstorder formula ϕ = ∃xψ(x) with ψ(x) constructed using ∧ and ∨ over atoms of the form E(t, t′ ) where t, t′ are variables from x or individual names from NI, and E is a path expression defined by the grammar

where r ∈ NR and A ∈ NC. A PEQ is a PRPQ that does not use the operators ∗ , ∪, and ◦ in path expressions. Equivalently, it is an FO formula ϕ = ∃xψ(x) where ψ is constructed using ∧ and ∨ over atoms r(t, t′ ) and A(t′ ) with t, t′ as above. An instance query (IQ) is just an expression of the shape C(a) for some concept C and a ∈ NI.

The semantics of PRPQs is defined via matches. Let us fix a PRPQ ϕ = ∃xψ(x) and an interpretation I. Let ind(ϕ) be the set of individual names in ϕ. A match for ϕ in I is a function π : x ∪ ind(ϕ) → ∆I such that π(a) = a, for all a ∈ ind(ϕ), and I, π |= ψ(x) under the standard semantics of first-order logic extended with a rule for atoms of the form E(t, t′ ). An interpretation I satisfies ϕ, written as I |= ϕ, if there is a match for ϕ in I.

A PRPQ ϕ is (finitely) entailed by a KB K, if I |= ϕ for every (finite) model I of K; we write K |= ϕ and K |=fin ϕ, respectively, in this case. Accordingly, we write K |= C(a) and K |=fin C(a) if a ∈ C I in all (finite) models I of K.

We study the corresponding decision problem-whether a given query is (finitely) entailed by a given KB-for different choices of knowledge base and query languages.

3 Tree-like Counter-Model Property

In this section we show a tree-like model property for SIQand SOQ: we show that if a query is not entailed by a KB, then there is a counter-model with a tree decomposition of bounded width and outdegree. For the automata-based decision procedure to yield optimal upper bounds, it is useful to consider canonical decompositions which we define next.

In canonical decompositions elements will be accompanied by certain key neighbors. Let us fix a KB K = (T , A). For an interpretation I, an element d ∈ ∆I , and r ∈ NtR , the r-cluster of d in I, denoted by QIr (d), is the set containing d and each e ∈ ∆I such that both (d, e) ∈ rI and (e, d) ∈ rI . This is the closest environment of d wrt. r. We also associate with d a larger set relIr (d) of r-successors relevant for the at-most restrictions of K. We let relIr (d) be the least set X such that QIr (d) ⊆ X and for all e ∈ X, f ∈ ∆I , and A ⊑ (⩽ n r B) in T , if e ∈ AI , f ∈ BI , and (e, f) ∈ rI ∗ , then QIr (f) ⊆ X. The construction of canonical decompositions relies on the following properties of relevant successors.

Lemma 1. For each r ∈ N t R , the following hold:

1. for all d, e ∈ ∆I , if e ∈ relIr (d) then relIr (e) ⊆ relIr (d);
2. if each r-cluster in I has size at most N, then for each d ∈ ∆I , |relIr (d)| ≤ N · 2poly(|T |) .

In a canonical tree decomposition, formalized in Definition 1 below, each non-root bag keeps track of all concepts and a single role indicated by r. Nominals are captured within a finite subinterpretation M represented faithfully in all bags; in the absence of nominals, one can take empty M and drop (C4). Conditions (C0)-(C3) ensure that apart from ∆M, neighboring non-root bags share a single element, sometimes accompanied by its relevant successors.

Definition 1. A tree decomposition T = (T, I) is canonical if

there exists r : T → NR ∪ {⊥} with r-1 (⊥) = {ε} such that

• (B0) for each w ∈ T, I(w) is a Σw-interpretation where Σε = NC ∪ N nt R and Σw = NC ∪ {r(w)} for w ̸= ε;
• (B1) for all v,w ∈ T, the restrictions of I(v) and I(w) to domain ∆v ∩ ∆w and signature Σv ∩ Σw coincide;
• (B2) for each v ∈ T \ {ε}, d ∈ F(v), and r ∈ N t R \ {r(v)}, a unique child w of v satisfies r(w) = r and d ∈ ∆w; and there is an interpretation Mwith nom(K) ⊆ ∆M ⊆ ∆ε, such that for each w ∈ T \ {ε} and its parent v, one has (C0) if r(w) ∈ N t R and v = ε, then ∆ε ⊆ ∆w;
• (C1) if r(w) ∈ N nt R , then ∆v ∩ ∆w = {d} ∪ ∆M for some d ∈ F (v);
• (C2) if r(v) ̸= r(w) ∈ N t R and v ̸= ε, then ∆w ∩ ∆v = {d} ∪ ∆M for some d ∈ F (v);
• (C3) if r(w) = r(v) = r ∈ N t R , then ∆v ∩∆w = rel I(v) r (d)∪ ∆M and rel I(v) r (d) = rel I(w) r (d) for some d such that either d ∈ F(v) or d ∈ F(u) and r(u) ̸= r(v) for the parent u of v; and
• (C4) if r(w) = r ∈ N t R , then rel I(w) r (d) = relMr (d) for all d ∈ ∆M.

Theorem 1. Let K = (T ,A) be a KB in normal form and ϕ a PRPQ with K ̸|= ϕ. If K is a SOQ KB or a SIQ- KB, then there exists a model J of T and A such that

• J has a canonical tree decomposition of width and outdegree poly(|ind(K)|) · 2poly(|T |) ; and
• J ∗ |= K and J ∗ ̸|= ϕ. 1

Proof. Let us fix a counter-model I for K and ϕ. We can assume that |QIr (d)| ≤ |ind(K)| + 2poly(|T |) for all d ∈ ∆I [Guti´errez-Basulto et al., 2018]. By Lemma 1, |relIr (d)| ≤ |ind(K)| · 2poly(|T |) for all d ∈ ∆I .

To build a canonical tree decomposition T, we unravel I starting from the interpretation of the ABox and then applying the extension rules (R0)-(R3) below, corresponding to conditions (C0)-(C3): (R0) collects relevant successors of the individuals in the ABox, (R1) performs standard unraveling of non-transitive roles, (R2) takes care of the change of roles, and (R3) realizes further unraveling of transitive roles.

More precisely, for the root bag, we take I restricted to the domain ind(A) ∪ ∆ and the signature NC ∪ N nt R , where ∆ is the union of relIr (a) for all a ∈ nom(K) and r ∈ N t R .

(R0) For each r ∈ N t R , we add as a child bag of ε the restriction of I to signature NC ∪ {r} and domain ⋃a∈ind(A) relIr (a) ∪ ∆ with each e /∈ ind(A) ∪ ∆ replaced by a fresh copy e′ . We call e the original of e′ .

1 Recall that in a model of the ABox or the TBox, the extensions of role names fromN t R need not be transitive.

Then, we use the following rules (R1)-(R3) ad infinitum, applying each rule only once to each previously added bag v. (R1) For each r ∈ N nt R , and each d′ ∈ F(v), let d ∈ ∆I be the original of d′ (possibly d = d′ ) and let W0 be the set of originals of all r-successors and r-predecessors of d′ in I(v). Pick a minimal set W ⊆ ∆I containing {d} ∪W0 ∪∆ such that for each s ∈ {r, r-} and A ⊑ (⩾ n s B) in T , if d ∈ AI , then d has at least n different s-successors in BI ∩W. For each e ∈ W \ (W0 \ ∆), add as a child bag of v the restriction of I to signature NC ∪ {r} and domain {d, e}∪∆ with all r-edges from ∆\{d} to {d, e}\∆ removed, d replaced by d′ and each f ∈ {e} \ ∆, by a fresh copy f ′ .

(R2) Assuming v ̸= ε, for each r ∈ N t R with r ̸= r(v), and each d′ ∈ F(v), let d be the original of d′ . Add as a child bag of v the restriction of I to signature NC ∪ {r} and domain relIr (d) ∪ ∆ where d is replaced by d′ and each e ∈ relIr (d) \ ({d} ∪ ∆), by a fresh copy e′ .

(R3) Assuming r(v) = r ∈ N t R , for each d′ ∈ ∆v fresh in v or in the parent u of v with r(u) ̸= r, let d be the original of d′ . Pick a minimal set W ⊆ ∆I containing relIr (d) ∪ ∆ such that for each A ⊑ (⩾ n r B) in T , if d ∈ AI , then d has at least n different r-successors in BI ∩W, and for each A ⊑ ∃r-.B in T , if d ∈ AI , then d has an r--successor in BI ∩W. For each e ∈ W \ (relIr (d) ∪∆), add as a child bag of v the restriction of I to the signature NC ∪{r} and domain relIr (e) ∪ relIr (d) ∪ ∆ where each element f ∈ relIr (d) \ ∆ is replaced by its copy f ′ from I(v), and each element f ∈ relIr (e) \ (relIr (d) ∪ ∆) by a fresh copy f ′ .

Let J be the interpretation underlying the resulting decomposition T. The function mapping each d′ ∈ ∆J to its original d ∈ ∆I gives a homomorphism from J to I, and consequently also from J ∗ to I. It follows that J ∗ ̸|= ϕ. Taking I restricted to ∆ as M, it is routine to check that T and J satisfy the remaining postulated properties. Note that while the construction is described for any normalized K, (R1) is correct only if K is either a SOQ KB or a SIQ- KB. Correctness of (R2) and (R3) follows from Lemma 1 (1).

4 PRPQEntailment for SIQ- and SOQ

We shall now exploit canonicity of tree decompositions in an automata-based decision procedure for query entailment in SIQ- and SOQ, yielding optimal complexity upper bounds.

Let us fix a (SIQ- or SOQ) KB K and a PRPQ ϕ, and denote with ΣC, ΣtR , Σnt R the concept names, transitive role names, and non-transitive role names used in K. By Theorem 1, if ϕ is not entailed by K, there exists a counter-model admitting a canonical tree decomposition of width and outdegree bounded by a constant N single exponential in |K|. We effectively construct a non-deterministic tree automaton recognizing such decompositions of counter-models, and thus reduce query entailment to the emptiness problem.

Let us introduce the necessary notions for tree automata. A k-ary Ω-labeled tree is a pair (T, τ) where T is a tree each of whose nodes has at most k successors and τ : T → Ω assigns a letter from Ω to each node. A non-deterministic tree automaton (NTA) over k-ary Ω-labeled trees is a tuple A = (Q,Ω, q0,Λ), where Q is a finite set of states, q0 ∈ Q is the initial state, Λ ⊆ ⋃i≤k (Q × Ω × Qi ) is a set of transitions. A run r on a k-ary Ω-labeled tree (T, τ) is a Q-labeled tree (T, r) such that r(ε) = q0 and, for every x ∈ T with successors x1, . . . , xm, there is a transition (r(x), τ(x), r(x1) · · · r(xm)) ∈ Λ. As usual, A recognizes the set of all Ω-labeled trees admitting a run.

Since counter-models have a potentially infinite domain, we encode tree decompositions of width N using a domain D of 2N elements, similar to what has been done, e.g., in [Gr¨adel and Walukiewicz, 1999]. Intuitively, if w is a successor node of v in the tree decomposition, then an element d occurring in (the bag at) w represents a fresh domain element iff d does not occur in v. More precisely, the alphabet Ω of the automaton is the set of all pairs (x, I) such that either x ∈ ΣR and I is a ΣC ∪ {x}-interpretation with ∆I ⊆ D, or x = ⊥ and I is a ΣC ∪ Σnt R -interpretation with ∆I ⊆ D.

Lemma 2. Given K, ϕ, and N, one can compute in time O(2poly(N) ) an NTA recognizing the set of encodings of canonical tree decompositions of width and outdegree at most N such that for the underlying interpretation J it holds that J ∗ |= K and J ∗ ̸|= ϕ, as well as J |= A and J |= T .

Proof. The desired NTA is the intersection of an NTA AK recognizing all canonical tree decompositions such that the underlying interpretation J satisfies J |= A, J |= T , and J ∗ |= K and an NTA A¬ϕ recognizing all tree decompositions of counter-models of ϕ. Since the latter is known from [Guti´errez-Basulto et al., 2018, Lemma 6], we concentrate on AK = (Q, Ω, q0, Λ), working over N-ary trees.

Informally, its construction relies on the following ideas: (i) by (B2) and (C2), in every bag there is at most one d satisfying the condition 'd ∈ F(u) . . . ' in Condition (C3); thus, (ii) canonicity can be checked by initially guessing M and then comparing neighboring interpretations and remembering the mentioned d in the states; (iii) J |= A can be verified by looking at labels of the root and its direct successors; (iv) due to canonicity and the TBox normal form, J |= T can be verified by looking at the current label (this suffices for at-most restrictions over transitive roles, due to canonicity) and possibly at successor bags (at-least restrictions, and atmost restrictions over non-transitive roles); (v) J ∗ |= T is a consequence of J |= T , by the normal form.

Formally, the set Q contains q0 and all tuples of the shape

where (x, I) ∈ Ω, F ⊆ ∆I , M is a ΣC ∪ Σnt R -interpretation with ∆M ⊆ D, B ⊆ A, C is a set of assertions of the shape (⩾ n s B)(d), (⩽ n s B)(d), or (∃s.B)(d) with d ∈ D, B ∈ ΣC, s a role in T , n ≤ N, and e, f ∈ D ∪ {ε}, r ∈ ΣtR .

In state q = 〈(x, I), F,M, B, C, e, r, f〉 reading symbol a = (x′ , I ′ ), the automaton allows a transition only in case the following conditions are satisfied:

• Conditions (B0)-(B2) and (C0)-(C4) with I, I ′ , x, x′ , F taking the role of I(v), I(w), r(v), r(w), F(v), respectively, and 'd ∈ F(u) . . . ' in (C3) replaced with 'd = f';
• x′ ̸= ⊥ and, if x = ⊥, then I ′ |= B;
• either e ̸= ε, e ∈ ∆I ′ , and r = x′ , or e = ε and x = x′ ;
• I ′ |= C(d) for all C(d) ∈ C with d ∈ ∆I ′ or C of shape (⩾ n s B) or ∃r-.B;

• I ′ |= α for all α ∈ T of the form di Ai ⊑ dj Bj, A ⊑ (⩽ n r B), and A ⊑ ∀r-.B.

In this case, Λ allows all transitions (q, a, q1 · · · qm), m ≤ N where each qi is of shape 〈(x′ , I ′ ), F ′ ,M, ∅, Ci, ei, ri, fi〉 with F ′ =∆I ′ \∆I and:

• for each d ∈ F ′ and each r ∈ ΣtR \ {x′ }, there is a unique i such that ei = d and ri = r; conversely, if ei ̸= ε for some i, then ei ∈ F ′ and ri ̸= x′ ;
• if e ̸= ε, then fi = e, for all i;
• for all A ⊑ ∃r-.B ∈ T and d ∈ AI ′ ∩ F ′ such that d /∈ (∃r-.B)I ′ , we have (∃r-.B)(d) ∈ Bi for some i;
• for all A ⊑ (⩽ n r B) ∈ T , r ∈ Σnt R , and d ∈ AI ′ ∩F ′ , there is a partition n = n0 + . . . +nm, such that d ∈ (⩽ n0 r B)I ′ , and (⩽ ni r B)(d) ∈ Ci, for all i;
• for all A ⊑ (⩾ n s B) ∈ T and d ∈ AI ′ ∩F ′ , there is a partition n = n0+. . .+nm, such that d ∈ (⩾ n0 s B)I ′ and (⩾ ni s B)(d) ∈ Ci, for all i with ni > 0.

The transitions for q0 are similar, but they additionally nondeterministically initialize M and check the non-transitive part of the ABox in the root, see the appendix. Correctness of the automaton is essentially a consequence of Points (i)-(v) mentioned above. It is routine to verify that AK is of the required size and can be constructed in the required time.

Recall that emptiness of NTAs can be checked in polynomial time. Thus, Lemma 2 together with the bounds on N from Theorem 1, yields a 2EXPTIME upper bound for PRPQ entailment in SIQ- and SOQ. A matching lower bound is inherited from positive existential query answering in ALC [Calvanese et al., 2014].

Theorem 2. PRPQ entailment over SIQ- and SOQ knowledge bases is 2EXPTIME-complete.

5 Finite PEQEntailment for SOQ

The goal of this section is to establish the following result.

Theorem 3. Finite PEQ entailment over SOQ knowledge bases is 2EXPTIME-complete.

The lower bound follows directly from the result on unrestricted query entailment for ALCO [Ngo et al., 2016], as the latter logic enjoys finite controllability. For the upper bound, we carefully adapt an approach previously used for SOF [Gogacz et al., 2018], which relies on the following additional condition imposed on tree-like counter-models.

Definition 2. A canonical tree decomposition is safe, if it contains no infinite downward path such that for each node w in this path, r(w) is the same transitive role name.

In what follows, by a counter-witness we understand a model of the ABox and the TBox whose transitive closure is a counter-model. The approach requires two ingredients: (1) equivalence of the existence of a finite counter-model and the existence of a counter-witness that admits a safe canonical tree decomposition, and (2) effective regularity of the set of safe canonical tree decompositions (of given width and outdegree) of counter-witnesses. For (2), observe that safety can be easily checked by an automaton with B¨uchi acceptance condition [Gr¨adel et al., 2002] and the number of states quadratic in the number of transitive role names in K: on each path the automaton remembers the role names associated with two most recently visited nodes; the state is accepting unless they are the same transitive role name. The product of this automaton and the one constructed in the previous section recognizes the desired language. Assuming (1) is also available, the upper bound follows like for the unrestricted case: the algorithm builds the automaton and tests its emptiness.

The reminder of this section provides (1). One implication is obtained via the following observation.

Lemma 3. If I is a finite interpretation of a SOQ KB, then the unravelling procedure from the proof of Theorem 1 yields a safe tree decomposition.

To prove the converse implication we begin from a carefully chosen counter-witness with a safe canonical tree decomposition. It is well known that each regular set of trees contains a regular tree, i.e., a tree with finitely many nonisomorphic subtrees. Hence, if there is a counter-witness with a safe canonical tree decomposition, there is also one with a regular safe canonical tree decomposition. Let T = (T, I) be such a tree decomposition of some counter-witness I, and let M be the interpretation guaranteed by Definition 1.

Let us restructure T by iteratively merging neighboring nodes associated to the same transitive role name: pick a node v with a child w such that r(v) = r(w) ∈ N t R , redefine I(v) as I(v)∪I(w), remove w from T, and promote all children of w to children of v. As a result we obtain a canonical tree decomposition S = (S, I) of I. By construction, S is strongly canonical: no neighboring nodes in S are associated with the same transitive role name. Hence, for each node w with parent v ̸= ε, ∆v ∩ ∆w \ ∆M = {dw} for some dw ∈ F (v).

Each regular safe tree decomposition has bounded length of downward paths of nodes associated with the same transitive role name. Consequently, the restructuring above keeps the outdegree and the width bounded.

Lemma 4. S has bounded degree and width.

We can now easily turn I ∗ into a finite model of K. Suppose that on each path of S, we fix a node v and its ancestor u (neither ε nor a child of ε) such that r(v) = r(u), I(v) ≃ I(u), and the witnessing isomorphism h maps dv to du and is identity over ∆M. Suppose also that for each element in ∆M, all witnesses required by at-least restrictions can be found among elements of ∆M and elements that do not occur in the subtrees of S rooted at the chosen nodes v. Note that for each path we can find such a pair of nodes, because the sizes of the bags are bounded in S. We shall modify I by removing parts of it and redirecting edges previously leading to the removed parts. Pick any path such that the corresponding dv has not been processed yet and has not been removed. Remove from I the union of ∆w with w ranging over descendents of v (including v), keeping only ∆M and dv. Replace each r(v)-edge leading from dv to a removed element e ∈ ∆v, with an r(v)-edge leading from dv to h(e). Repeat until no such path exists. The resulting interpretation J is obviously finite. Checking correctness is routine.

Lemma 5. J ∗ |= K .

To ensure that J ∗ ̸|= ϕ we need to choose the nodes v and u more carefully. Relying on ϕ being a PEQ, not an arbitrary PRPQ, we apply the colored blocking principle [Gogacz et al., 2018]: to keep u and v sufficiently similar and sufficiently far apart, we look at their neighborhoods of sufficiently large radius and use additional coloring to distinguish elements within each neighborhood (see Appendix for details).

6 IQEntailment

We also get the following results on IQ entailment.

Theorem 4. Finite and unrestricted IQ entailment is CONEXPTIME-complete over SOQ KBs. Unrestricted IQ entailment over SIQ- KBs and finite IQ entailment over SIQ- KBs restricted to a single transitive role and no nontransitive roles is 2EXPTIME-complete.

Proof. As is well-known, (finite) IQ entailment reduces to the complement of (finite) KB satisfiability; we focus on the latter. For SOQ, we simply use the facts that (finite) KB satisfiability for SOQ is NEXPTIME-complete [Guti´errez-Basulto et al., 2017] and that the lower bound holds in the finite [Kazakov and Pratt-Hartmann, 2009].

The 2EXPTIME upper bound for unrestricted KB satisfiability follows from Theorem 2, and for finite satisfiability in the above fragment of SIQ- follows from Theorem 2 and a recent result by Bednarczyk et al. [2019], implying that satisfiability and finite satisfiability coincide for this fragment of SIQ- . This approach cannot be generalized to full SIQsince SIQ- lacks the finite model property.

We next show that these upper bounds are tight by reducing the word problem for 2n -space bounded alternating Turing machines (ATMs), which is known to be 2EXPTIMEhard [Chandra et al., 1981]. An ATM M = (Q, Θ, Γ, q0, ∆) consists of the set Q of states partitioned into existential states Q∃ and universal states Q∀, the input alphabet Θ, the tape alphabet Γ, the starting state q0 ∈ Q∃, and the transition relation ∆. Without loss of generality, we assume that each of M's configurations has exactly two successor configurations, universal and existential states alternate, and M accepts a word iff there is an infinite (alternating) run.

Given M, w, we construct in polynomial time a knowledge base K = (T , {I(a0)}) using a single transitive role name r such that M accepts w iff K is satisfiable. We represent configurations of size 2n in the leaves of binary trees of depth n. To this end, we use concept names X0, . . . , Xn-1 (representing bits of an exponential counter) and L0, . . . ,Ln (for the levels of the tree), and include the following CIs for all i, j with 0 ≤ i < n and i < j ≤ n:

It should be clear that every model of L0 and these CIs contains a full binary tree of depth n such that the leaves, that is, the elements satisfying Ln, correspond to the numbers 0, . . . , 2n - 1 in the natural way, via concept names Xi. Let Σ = Γ ∪ (Q × Γ) be the set of possible labels of a cell in M's computation, and introduce concept names C x σ for every σ ∈ Σ, x ∈ {l, h, r}. Every leaf with number i is labeled with three concepts C lσ1 ,C h σ2 ,C rσ3 representing the cells i - 1, i, i + 1 of a configuration using the CI:

We use these trees as follows. The concept name I enforces a skeleton structure modeling an alternating computation using the following CIs, for i ∈ {1, 2}:

Thus, every model of I contains the following structure, where every triangle represents one of the described trees, and A∀ (Ai∃ ) marks universal (existential) configurations:

It remains to ensure that (i) the leaf labeling in every tree is actually a configuration, (ii) neighboring trees describe successor configurations, and (iii) the first tree is labeled with the initial configuration. We concentrate on (ii), as (i) is similar and (iii) is straightforward. We illustrate the idea on T1 and T2 in the figure. In T1, we enforce in every leaf an r-successor satisfying the label of that cell in the successor configuration (computable from the C x σ ). In T2, we enforce in every leaf an r-successor with the current label C h σ . Both in T1 and T2, these additional elements satisfy a fresh concept name S and have the same counter value as in the leaves. Observe that, by transitivity, all 2·2n created nodes are 'visible' from d satisfying B∃ in the figure. By including the CI B∃ ⊑ (⩽ 2n r S), S-elements with the same counter value from T1 and T2 are forced to identify, thus achieving the desired synchronization. Having (i)-(iii) in place, it is routine to show that K is satisfiable iff M accepts w. The lower bound applies to finite satisfiability, since K is satisfiable iff it is finitely satisfiable.

7 Outlook

This paper makes a step towards a complete picture of query entailment in DLs with number restrictions on transitive roles. There are several natural next steps involving finite entailment. The first is to cover full SIQ- . Amore challenging goal is to go beyond instance queries: an immediate obstacle is that the natural safety condition for SIQ- does not guarantee strongly canonical decompositions. Covering full PRPQs even just for SQ seems to require generalizing the colored blocking principle, or finding an entirely different tool.

Acknowledgments

Gogacz and Murlak were funded by Poland's National Science Centre grant 2018/30/E/ST6/00042, Ib´a˜nez-Garc´ıa by ERC Starting grant 637277 FLEXILOG, and Jung by ERC Consolidator grant 647289 CODA. This work was also supported by the OeAD WTZ project PL 15/2017.