Data Complexity in Expressive Description Logics with Path Expressions

1 Introduction

Formal ontologies are essential in nowadays approaches to safe and trustworthy symbolic AI, serving as the backbone of the Semantic Web, peer-to-peer data management, and information integration. Such applications often resort to managing and reasoning about graph-structure data. A premier choice for the reasoning framework is then the well-established family of logical formalisms known as description logics (DLs) [Baader et al., 2017] that underpin the logical core of OWL 2 by the W3C [Hitzler et al., 2012]. Among the plethora of various features available in extensions of the basic DL called ALC, an especially prominent one is ·reg, supported by the popular Z-family of DLs [Calvanese et al., 2009]. Using ·reg, one can specify regular path constraints and hence, allow the user to navigate the underlying graph data-structure. In recent years, many extensions of ALCreg for ontology-engineering were proposed [Bienvenu et al., 2014; Calvanese et al., 2016; Ortiz and Simkus, 2012], and the complexity of their reasoning problems is mostly well-understood: Calvanese et al. [2009; 2016]; Bednarczyk et al. [2019; 2022].

Vardi [1982] observed that measuring the user's data and the background ontology equally is not realistic, as the data tends to be huge in comparison to the ontology. This gave rise to the notion of data complexity: the ontology (TBox) is fixed upfront and only the user's data (ABox) varies. The satisfiability problem for DLs is usually NP-complete w.r.t. the data complexity, including the two-variable counting logic [PrattHartmann, 2009] (encoding DLs up to ALCBIOQSelf) as well as SROIQ [Kazakov, 2008], the logical core of OWL2. Regarding DLs with path expressions, NP-completeness of ALCI Self reg [Jung et al., 2018] was established only recently.

1.1 Our Main Contribution and a Proof Overview

We study the data complexity of the satisfiability problem for decidable sublogics of ZOIQ (a.k.a. ALCHb Self reg OIQ), and establish NP-completeness of ZIQ, ZOQ, and ZOI. As all the mentioned DLs possess the quasi-forest model property (i.e. every satisfiable knowledge-base (KB) has a forestlike model), for the uniformity of our approach we focus on the satisfiability of ZOIQ over quasi-forests. Calvanese et al. [2009] proved that quasi-forest-satisfiability of ZOIQ is EXPTIME-complete w.r.t. the combined complexity. Unfortunately, their approach is automata-based and relies on an internalisation of ABoxes inside ZOIQ-concepts, and thus cannot be used to infer tight bounds w.r.t. the data complexity.

We employ the aforementioned algorithm of Calvanese et al. as a black box and design a novel algorithm for quasi-forestsatisfiability of ZOIQ-KBs. In our approach we construct a quasi-forest model in two steps, i.e. we construct its root part (the clearing) separately from its subtrees. Our algorithm first pre-computes (an exponential w.r.t. the size of the TBox but of constant size if the TBox is fixed) set of quasi-forestsatisfiable ZOIQ-concepts that indicate possible subtrees that can be "plugged in" to the clearing of the intended model. Then it guesses (in NP) the intended clearing and verifies its consistency in PTIME based on the pre-computed concepts and roles. For the feasibility of our "modular construction" a lot of bookkeeping needs to be done. Most importantly, certain decorations are employed to decide the satisfaction of automata concepts and number restrictions by elements in an incomplete and fragmented forest. The first type of decorations, given an automaton A, aggregates information about existing paths realising A and starting at one of the roots of the intended model. As a single such path may visit several subtrees, we cut such paths into relevant pieces and summarise them by means of "shortcut" roles and ZOIQ-concepts describing paths fully contained inside a single subtree. The second type of decorations "localise" counting in the presence of nominals, as the nominals may have successors outside their own subtree and the clearing. These two "small tricks", obfuscated by various technical difficulties, are the core ideas underlining our proof. We conclude the paper by presenting how our algorithm can be adapted to the entailment problem of rooted queries over ZIQ. The key idea here is to guess an "initial segment" of a quasi-forest with no query match, and check if it can be extended to a full model of the input KB.

2 Preliminaries

We assume familiarity with description logics (DLs) [Baader et al., 2017], formal languages, and complexity [Sipser, 2013]. We fix countably-infinite pairwise-disjoint sets NI, NC, NR of individual, concept, and role names. An interpretation I := (∆I , ·I ) consists of a non-empty domain ∆I and a function ·I that maps a ∈ NI to aI ∈ ∆I , A ∈ NC to AI ⊆ ∆I , and r ∈ NR to r I ⊆ ∆I ×∆I . The set of simple roles NspR is defined with the grammar s ::= r ∈ NR | s - | s∩s | s∪s | s\s. Simple roles are interpreted as expected by invoking the underlying set-theoretic operations, e.g. I interprets (r ∪ (s \ t))- as the inverse of (r I ∪(s I \ t I )). The superscripts ∗ and + denote the Kleene's star and plus, while · denotes concatenation. A path in I is a word ρ := ρ1 . . . ρ|ρ| in (∆I )+ such that for all i < |ρ| there is a role name r ∈ NspR with (ρi, ρi+1) ∈ r I .

Automata. We use nondeterministic automata (NFAs). For states q and q′ of an NFAA, Aq,q′ denotes the corresponding NFA with the initial (resp. final) state switched to q (resp. q′ ). NFAs use roles from NspR and tests C? for concepts C as alphabet. A path ρ realises A (ρ |= A, ρ is an A-path) if A accepts some word w1r1 . . . w|ρ|-1r|ρ|-1w|ρ|, where ri ∈ NspR and wi are (possibly empty) sequences of tests, satisfying (ρi, ρi+1) ∈ r I i and ρi ∈ CI for all i ≤ |ρ| and tests C? in wi.

Expressive DLs. The DL ZOIQ [Calvanese et al., 2009] is the main object of our study. For all A ∈ NC, s ∈ NspR, o ∈ NI, n ∈ N and NFA A, we define ZOIQ-concepts C with:

We define the DLs ZOI, ZIQ, and ZOQ, respectively, by dropping (a) number restrictions, (b) nominals, and (c) role inverses from the syntax of ZOIQ. W.l.o.g. we allow for regular expression (with tests) in place of NFAs in above syntax.

A ZOIQ-KB K := (A, T ) is composed of two sets of axioms, an ABox A and a TBox T . An interpretation I is a model of K (I |= K) if it satisfies all the axioms of K. The content of ABoxes and TBoxes, as well as the notion of their satisfaction is defined below, assuming that a,b ∈ NI, A ∈ NC, r ∈ NR, s , t ∈ NspR, and C, D are ZOIQ-concepts.

Note that ABoxes do not involve complex concepts. Otherwise, data complexity of ALCreg is already EXPTIME-hard.

A TBox is in Scott's normal form if its axioms have the form:

for A, B, B′ ∈ NC∪{⊤, ⊥}, o ∈ NI, r ∈ NR, s ∈ NspR, n ∈ N, and NFAs Aq,q′ . Here I |= C ≡ D iff CI = DI . W.l.o.g. we focus only on KBs with TBoxes as above [Appendix B].

Queries. We focus on conjunctive queries (CQs) defined by the grammar: q ::= A(x) | r(x, y) | q ∧q, where A ∈ NC, r ∈ NR, and x , y being either variables or individual names. An interpretation I satisfies a query q (I |= q), if there is an assignment η (a match, defined as expected), mapping variables to domain elements and individual names a ∈ NI to the corresponding aI , under which q evaluates to true. A CQ is rooted if it has at least one individual name and its query graph is connected. A KB entails q if every of its models satisfies q.

Problems. Let DL be a logic, and Q be a class of queries. In the satisfiability problem we ask if a given DL-KB K := (A, T ) has a model. In the (rooted) query entailment problem we ask if a given DL-KB K entails a (rooted) query q ∈ Q. We distinguish two ways of measuring the size of the input, which gives rise to combined and data complexity. In the first case all the components A, T and q equally contribute to the size of the input. In the second case, T and q are assumed to be fixed beforehand, and thus their size is treated as constant.

Forests. We adapt the notion of quasi-forests [Calvanese et al., 2009] under the standard set-theoretic reconstruction of the notion of an N-forest as a prefix-closed subset of N+ without ε. Our notion is stricter than the original definition by Calvanese et al. but the differences are negligible [Appendix C].

Definition 1. LetNAI andNTI be finite subsets ofNI, Root ∈ NC, and child, edge, id ∈ NR. An interpretation I is an (NAI ,NTI )-quasi-forest if its domain ∆I is an N-forest,

and for all roles r I and all pairs (d, e) ∈ r I at least one of the conditions hold: (i) both d and e belong to RootI , (ii) one of d or e is equal to oI for some name o ∈ NTI , (iii) (d, e) ∈ id I ∪ child I ∪ (child -)I . For convenience, we refer to pairs (d, e) ∈ r I satisfying the second condition as backlinks, and the ones satisfying (d, e) ∈ id I as self-loops. The clearing of I is the restriction of I to RootI . A quasi-forest is N-bounded if every domain element has at most N child-successors. ◀

The names fromNTI are dubbed nominals, and will be usually denoted with decorated letters o. Their interpretations are usually referred as nominal roots. Throughout the paper we employ suitable notions from graph theory such as node, root, child, parent, or descendant, defined as expected in accordance with ∆I , child I and RootI . For instance, d is a descendant of c whenever (c, d) ∈ (child I )+ holds. Consult Example 1.

The element 1 has a unique child 10. The roots of I are 0, 1, 2, and 3. The nominal roots are 1,2, and 3. The pairs (1, 001), (2000, 1), and (3, 20) are example backlinks. ◀

A quasi-forest model of a ZOIQ-KB K := (A, T ) is an (ind(A), ind(T ))-quasi-forest satisfying K, where ind(A) and ind(T ) are sets of all individual names from A and T . The results by Calvanese et al. [2009, Prop. 3.3] and Ortiz [2010, L. 3.4.1, Thm. 3.4.2] advocate the use of quasi-forest models.

Lemma 1. Let K:=(A, T ) be a KB of ZOQ, ZOI, or ZIQ. Then is an integer N (exponential w.r.t. |T |) such that: (I) K is satisfiable iff K has an N-bounded quasi-forest model, and (II) for all (unions of) CQs q, we have K ̸|= q iff there exists an N-bounded quasi-forest model of K violating q. ◀

The quasi-forest (counter)models of ZOIQ-KBs are canonical if they are N-bounded for the N guaranteed by Lemma 1. Hence, for the deciding the satisfiability and query entailment over ZIQ, ZOQ, and ZOI, only the class of canonical quasi-forest models is relevant. We say that a ZOIQ-KB is quasi-forest satisfiable whenever it has a canonical quasiforest model. The quasi-forest satisfiability problem is defined accordingly. We have [Ortiz, 2010, L 3.4.1, Thm. 3.4.2] that:

Lemma 2. The quasi-forest satisfiability problem for ZOIQKBs is EXPTIME-complete (w.r.t. the combined complexity). In particular, the satisfiability of ZIQ, ZOQ, and ZOI-KBs is EXPTIME-complete (w.r.t. the combined complexity). ◀

3 Basic Paths in Quasi-Forests

The main goal of this section is to provide a characterisation of how paths in quasi-forests look like and how they can be decomposed into interesting pieces. A path ρ in I is nameless if it does not contain any named elements (i.e. no element of ρ has the form aI for some a ∈ NI). Similarly, ρ is called an a-subtree path if all the members of ρ are descendants of aI . In quasi-forests, nameless paths are precisely subtree paths.

Definition 2. Let I be an (NAI ,NTI )-quasi-forest, a,b ∈ (NAI ∪NTI ), o,¨ o ∈ NTI , and ρ be a path in I. We call ρ:

• (a,b)-direct if ρ =aI ·bI .
• a-inner if ρ =aI ·¯ ρ for some a-subtree path ¯ ρ.
• a-roundtrip if ρ =aI ·¯ ρ·aI for some a-subtree path ¯ ρ.
• (a,o)-inout if ρ = ¯ ρ·oI for some a-inner path ¯ ρ.
• (a,o)-outin if the reverse of ρ is (a,o)-inout.
• (a,o)-inner if ρ =oI ·¯ ρ for some a-subtree path ¯ ρ.
• (a,o,¨ o)-bypass if ρ = oI ·¯ ρ·¨ oI for an a-subtree path ¯ ρ.

If ρ falls into one of the above seven categories, we call ρ basic. Paths ρ := ¯ ρ·d for a nameless ¯ ρ and a root d are called outer. Finally, ρ is decomposable whenever there exists a growing sequence of indices i1 < i2 < . . . < ik with i1=1 and ik=|ρ| such that for all j < k the path ρij . . . ρi(j+1) is basic. ◀

By a careful analysis of Definitions 1-2 we can show:

Observation 1. Take I, a, b, ρ as in Definition 2. If ρ has the form aI · ¯ ρ or aI · ¯ ρ·bI for a nameless ¯ ρ then ρ is basic. ◀

We can now employ Observation 1 and invoke the induction over the total number of named elements in ρ to establish:

Lemma 3. If I is a quasi-forest then every path starting from a named element is decomposable. ◀

Basic paths are expressible in ZOIQ by means of regular expressions with tests. Their construction involves nominal tests {a}?, "descendant of a" tests ∃(child -)+.{a}?, and role names edge, child. For instance, all (a,o,¨o)-bypasses match:

Lemma 4. Let τ be a "category" of paths from Def. 2 (including nameless and outer paths). There is an NFA Aτ (using testing involving only individual names mentioned in τ) that realises for all quasi-forests I exactly the paths of the category τ. Moreover, for any regular language L (given as an NFA B or a reg-exp R) there exists an NFA (B ▷◁ Aτ ) (resp. (R ▷◁ Aτ)) of size polynomial in |B| (resp. |R|) that realises precisely the paths in I of category τ realising B (resp. R). ◀

4 Automata Decorations

Overview. We use Lem. 3 to devise a method of decorating the clearing of I with extra information about the basic paths realising an NFA A. This helps to decide the satisfaction of concepts ∃A.⊤ in quasi-forests in a modular way, independently for the clearing of a quasi-forest and its subtrees. Note:

Fact 1. Let d ∈ (∃A.⊤)I for an NFAA and an (NAI ,NTI )- quasi-forest I. There is an A-path ρ starting from d s.t.: (a) d is a root, (b) ρ is nameless, or (c) ρ = ¯ ρ· ˆ ρ for some outer ¯ ρ. ◀

Given an NFA A with the state set Q, by the A reachability concepts C⇝(A) we mean the set {ReachA q,q′ | q, q′ ∈ Q}. Ideally, ReachA q,q′ should label precisely the roots of quasiforests satisfying ∃Aq,q′ .⊤. With Lemma 5 we explain the desired "modularity" condition. It simply says that if ReachA q,q′ - concepts are interpreted as desired, then the verification of whether an element d satisfies ∃Aq,q′ .⊤ boils to (i) testing whether d is labelled with ReachA q,q′ if d is a root, or (ii) testing existence of a certain path which fully contained in the subtree of d, possibly except the last element which can also be the root of d or a nominal. We rely on the NFAs Anmls and Aoutr from Lemma 4 that detect nameless and outer paths.

Lemma 5. Let A be an NFA with the set of states Q, and let I be an (NAI ,NTI )-quasi-forest that interprets all ReachA q,q′ - concepts from C⇝(A) equally to Root ⊓∃Aq,q′ .⊤. Then for all states q, q′ ∈ Q, the concept ∃Aq,q′ .⊤ is interpreted in I equally to the union of concepts:

• Root ⊓Reachq,q′ , · ¬Root ⊓ ∃(Aq,q′ ▷◁ Anmls ).⊤, and
• ¬Root ⊓ ⊔ˆq∈Q ∃(Aq,ˆq ▷◁ Aoutr ). (Root ⊓Reachˆq,q′ ). ◀

Let rel(NTI ,Aq,q′) denote the above concept union, called the NTI -relativisation of ∃Aq,q′ .⊤. We say that d ∈ ∆I virtually satisfies ∃Aq,q′ .⊤ whenever d satisfies rel(NTI ,Aq,q′). Thus, Lemma 5 tells us that under some extra assumptions the notion of satisfaction and virtual satisfaction coincide.

Decorations. In what follows, we define ZOIQ-concepts and roles, dubbed automata decorations, intended to guarantee the desired interpretation of the reachability concepts.

Definition 3. Given an NFAA with the state-set Q, the set of (NTI ,A)-concepts C(NTI ,A) is composed of the following concept names (for all states q, q′ ∈ Q and names o, ¨ o ∈ NTI ):

A quasi-forest I properly interprets C(NTI ,A) if CI = {aI | a ∈ NI, cond(C, a)} for concepts and conditions as below.

The size of C(NTI ,A) is clearly polynomial in |A|·|NTI |. ◀

The concepts from C(NTI ,A) "bookkeep" the information about relevant basic paths realising NFA starting from a given root. Throughout the paper, we employ a fresh individual name (the ghost variable), to stress that the constructed concepts are independent fromNAI . With C[ /a] we denote the result of substituting a for all occurrences of in C. Relying on NFAs from Lemma 4, we construct ZOIQ-concepts that describe the intended behaviour of (NTI ,A)-concepts. For instance, RTA q,q′ is defined as ∃(Aq,q′ ▷◁ A -roundtrip ).⊤.

Lemma 6. For all C fromC(NTI ,A), there exists a ZOIQconcept desc(C) (of size polynomial w.r.t. |A|·|NTI |) that uses only individual names fromNTI ∪{ } with the property that "for all (NAI ,NTI )-quasi-forests I and a ∈ NI we have: ..cond(C,a) is satisfied in I iff aI is in (desc(C)[ /a])I ."◀

We next invoke Lemma 6 to rephrase the notion of proper interpretation of C(NTI ,A) in the language of satisfaction of ZOIQ-concepts by the clearings of quasi-forests. We have:

The information provided by the proper interpretation of (NTI ,A)-concepts is not sufficient to ensure the proper interpretation of the reachability concepts by the clearings of quasi-forests. The main reason is that the concepts from (NTI ,A) concern only about the basic paths. As some automata constraints cannot be satisfied by basic paths, e.g. ∃({o}?edge{¨o}?edge{ˇo}?).⊤, more work needs to be done. To be able to compose basic paths into bigger pieces, another "layer of decoration" is needed: this time with fresh roles representing the endpoints of basic paths from Definition 2, as summarised by Figure 1. For instance, whenever there is an (a,o)-inout ρ realisingAq,q′ in a quasi-forest I, the roots aI and oI are going to be linked by the role io A,o q,q′ (and similarly for other categories of basic paths that start and end in roots). Such roles can be seen as "aggregated paths". The "aggregated paths" will be unfolded afterwards into real paths, and the satisfaction of automata constraints by them will be verified by means of the guided automata (introduced in Definition 5). However, there exist cases of basic paths where the last element is unnamed, more precisely (a,o)-inner and a-inner paths. In their cases we treat aI as the "virtual end" of ρ (and hence we link aI and oI ). To ensure that such an "aggregated path" can no longer be extended, we decorate the corresponding role with the dead-end symbol skull. When constructing the guided automaton, the roles carrying skull will lead to states with no outgoing transitions (dead ends).

Definition 4. Given a PSA A with the state-set Q, the set of (NTI ,A)-roles R(NTI ,A) is composed of the following role names (for all states q, q′ ∈ Q and names o, ¨ o ∈ NTI ):

An (NAI ,NTI )-quasi-forest I properly interprets R(NTI ,A) if its roles consist of pairs p of roots of I as indicated below.

The size of R(NTI ,A) is polynomial w.r.t. |A|·|NTI |. ◀

We stress that we interpreted role names from R(NTI ,A) based on the concepts fromC(NTI ,A) rather than on the existence of certain paths realising A. This allows us to verify their proper interpretation, independently from the verification of the proper interpretation of C(NTI ,A)-concepts. The roles fromR(NTI ,A) can be seen as "shortcuts" aggregating fragments of runs of A. To retrieve the runs, we invoke the A-guided automaton that operates solely on such "shortcuts".

Definition 5. For an NFA A with the state-set Q, we define the A-guided NFA B. The set of states Q′ of B consists of all q ∈ Q and their fresh copies qskull. The transitions in B have the form (q, r, q′ ) for all q, q′ ∈ Q′ , and all r from R(NTI ,A) labelled with the ordered pair (q, q′ ). By design, all states decorated with skull have no outgoing transitions. ◀

The guided automaton B is of size polynomial in |A|·|NTI |, and it traverses only the clearings of quasi-forests. The following Lemma 7 reveals the desired property of B.

Lemma 7. Let A be an NFA with an A-guided NFA B, and I be an (NAI ,NTI )-quasi-forest that properly interprets C(NTI ,A) and R(NTI ,A). For all states q, q′ of A: (Root ⊓ ∃Aq,q′ .⊤)I = (Root ⊓ (∃Bq,q′ .⊤ ⊔ ∃Bq,q′skull .⊤))I . ◀

Its proof relies on either (a) shortening a path ρ |= Aq,q′ to its subsequence composed of all named elements, or (b) replacing any two consecutive elements in ρ |= Bq,q′ with the corresponding paths guaranteed by the roles from Def. 4.

Example 2. Let ρ := aI ·oI ·ρ1·oI ρ2·¨ oI ·ρ3 |= Aq1,q5 be a path in a quasi-forest I (depicted below), and A be an NFA with states indicated by decorated q. Suppose (i) aI ·oI |= Aq1,q2 is (a,o)-direct, (ii) oI ·ρ1·oI |= Aq2,q3 is an oroundtrip, (iii) oI ρ2·¨ oI |=Aq3,q4 is an (b,o,¨ o)-bypass, and (iv) ¨ oI ·ρ3 |=Aq4,q5 is (c,¨ o)-inner. So, aI ∈ (∃Aq1,q5 .⊤)I .

With the proviso that a quasi-forest I properly interprets both C(NTI ,A) and R(NTI ,A), Lemma 7 guarantees the desired interpretation of reachability concepts ReachA q,q′ .

Definition 6. Let I,A,B be as in Lemma 7, and Q be the state-set of A. The set of A-reachability-concepts C⇝(A) is {ReachA q,q′ | q, q′ ∈ Q}. I properly interprets C⇝(A) if

for all q, q′ ∈ Q. We call I virtually (NTI ,A)-decorated if it properly interprets R(NTI ,A), and C⇝(A), and (NTI ,A)- decorated if it additionally properly interprets C(NTI ,A). ◀

Relying on Lemma 5 and Lemma 7 we can show:

Lemma 8. Let A be an NFA, and let I be an (NTI ,A)- decorated (NAI ,NTI )-quasi-forest. For all elements d in I, if d virtually satisfies ∃Aq,q′ .⊤ then d satisfies ∃Aq,q′ .⊤.

We conclude by showing an algorithmic result concerning (virtually) (NTI ,A)-decorated quasi-forests. It exploits the fact that the regular path queries over databases can be evaluated in PTIME [Mendelzon and Wood, 1995, Lemma 3.1].

Lemma 9. Let I be a finite interpretation with RootI = ∆I , and A be an NFA. We can then verify in time polynomial w.r.t. (|A|·|I|) whether I is virtually (NTI ,A)-decorated. ◀

Lemma 9 tells us that if I is the clearing of some (NAI ,NTI )- quasi-forest J that properly interprets C(NTI ,A)-concepts, then we can verify if J is (NTI ,A)-decorated in PTIME.

5 Counting Decorations

We want to "relativise" number restrictions in the presence of nominals, so that in the suitably decorated quasi-forest models, the satisfaction of concepts of the form (≥n r).⊤ by the clearing can be decided solely based on the decoration of the clearing. Observe that for a given a root d of a quasi-forest I and a role name r , the set of r-successors of d can be divided into three groups: (a) the clearing, (b) the children of d, and (c) the descendants of roots (but only in case d is a nominal root). To relativise counting, we decorate each element of the clearing with the total number of their r-successors in categories (a) and (b), as well as the information, for each nominal o, on (c) how many of their descendants are r -successors of o.

Definition 7. Fix r ∈ NR, n ∈ N, and a finiteNTI ⊆NI. The set of (NTI ,≥n r)-counting-concepts C#(NTI ,≥n r) consists of concept names Clrngr t , Chldr t ,Desr,o t foro ∈ NTI and thresholds t of the form "=m" for 0 ≤ m ≤ n or "≥n+1". All integers appearing in thresholds are encoded in binary. An (NAI ,NTI )-quasi-forest I is (≥n r)-semi-decorated if all roots d have unique thresholds tdcl , tdch , and td o for all o ∈ NTI , for which d satisfies the concept

The above concepts are called the (NTI ,≥n r)-descriptions of d. Note that their size is polynomial w.r.t. |NTI |· log2(n).◀ Similarly to the previous section, we next introduce the notion of proper satisfaction. Intuitions regarding Definition 7 are provided in Example 3. We encourage the reader to read it.

Definition 8. An (NAI ,NTI )-quasi-forest I properly interprets C#(NTI ,≥n r) if I is (≥n r)-semi-decorated and for all roots aI of I and o ∈ NTI , the root aI belongs to:

• (Clrngr t )I iff |{d: d ∈ RootI , (aI , d) ∈ r I }| t,
• (Chldr t )I iff |{d: (aI , d) ∈ r I , (aI , d) ∈ child I }| t,
• (Desr,o t )I ifif |{d: (oI , d) ∈ r I , (aI , d) ∈ (child +)I }| t. In this case we also say that I is (≥n r)-decorated. ◀

Based on the above definitions, we can easily express the intended behaviour of C#(NTI ,≥n r)-concepts in ZOIQ, using (=n r ).C as an abbreviation of (≥n r ).C⊓¬(≥n+1 r ).C. In the most difficult case, we describe (Desr,o =42 )I with:

Lemma 10. For every (NTI ,≥n r)-description C there is a ZOIQ-concept desc(C) (of size polynomial w.r.t. |C|) that uses only individual names fromNTI ∪ { } for a fresh , s.t. for all (NTI ,≥n r)-semi-decorated (NAI ,NTI )-quasi-forests I: I is (≥n r)-decorated iff for every root aI of I and its (NTI ,≥n r)-description Cwe haveaI ∈ (desc(C)[ /a])I .◀

Example 3. Let us consider an ({a,b}, {o})-quasi-forest I sketched below and a role name r depicted as a green arrow. As suggested by the drawing, (i) aI has no r-successors among the clearing of I and precisely one r -successor among its children, (ii) oI has two r-successors among the clearing of I, it has precisely two r-successor among its children, one r -successor that is a descendant of aI , and three r -successors that are descendants of bI , and (iii) bI has precisely one rsuccessor inside the clearing of I and no other r-successors.

Suppose now that I is ({o},≥2 r)-decorated. This implies:

• aI ∈ (Clrngr=0 ⊓Chldr=1 ⊓Desr,o =1 )I .
• oI ∈ (Clrngr=2 ⊓Chldr=2 ⊓Desr,o =2 )I .
• bI ∈ (Clrngr=1 ⊓Chldr=0 ⊓Desr,o ≥2+1 )I .

◀

Lemma 10 rephrases the notion of proper satisfaction in the language of ZOIQ-concepts. Call a quasi-forest I virtually (NTI ,≥n r)-decorated if I is (NTI ,≥n r)-semi-decorated and properly interprets concepts of the form Clrngr t . We have:

Lemma 11. For a finite interpretation I we can test in polynomial time w.r.t. |I| if I is virtually (NTI ,≥n r)-decorated. ◀

We use the numbers appearing in (NTI ,≥n r)-descriptions labelling the roots of (≥n r)-decorated quasi-forests to decide the satisfaction of (≥n r).⊤. We first describe it with an example. Suppose that we want to verify if a non-nominal root d from I satisfies (≥3 r) based on its labels Clrngr=1 and Chldr≥3+1 . It suffices to check if 1 + (3 + 1) is at least 3. For the nominals roots o, we additionally take all the concepts Desr ,o t into account, that are spread across the whole clearing.

An element d from a finite I virtually satisfies (≥n r).⊤, whenever d satisfies (≥n r).⊤ in every (≥n r)-decorated (NAI ,NTI )-quasi-forest with the clearing equal to I. We show:

Lemma 12. For a finite virtually (NTI ,≥n r)-decorated interpretation I with ∆I = RootI and d ∈ RootI we can test in time polynomial in |I| if d virtually satisfies (≥n r).⊤. ◀

6 Elegant Models and Their Summaries

In this section we benefit from various decorations introduced in the previous sections to design a succinct way of representing quasi-forest models of ZOIQ-KBs, dubbed summaries. From now on we will focus only on KBs in Scott's normal form (i.e. with TBoxes in Scott's normal form) and on certain class of elegant models introduced in Definition 9.

Definition 9. Let K := (A, T ) be a ZOIQ-KB in Scott's normal form and let I be its model.

We call I elegant if it satisfies all the conditions below:

• (i) I is a canonical quasi-forest model of K,
• (ii) I is (ind(T ),≥n r)-decorated for all number restrictions (≥n r).⊤ from T ,
• (iii) I is (ind(T ),A)-decorated for all automata A from T ,
• (iv) I interprets all concept and role names that do not appear in K, the set {Root, edge, child, id}, and in mentioned decorations, as the empty set. ◀

Invoking the normal form lemma [Appendix A], Lemma 1, as well as the definitions of proper interpretation, we obtain:

Lemma 13. For every ZOIQ-TBox T we can compute in PTIME a ZOIQ-TBox T ′ in Scott's normal form that possibly such that for every ABox A we have: (i) (A, T ) is quasiforest satisfiable iff (A, T ′ ) has an elegant model, and (ii) for every UCQ q using only concepts and roles present in T we have that (A, T ) has a canonical quasi-forest model violating q iff (A, T ′ ) has an elegant model violating q. ◀

To-be-defined summaries are nothing more than ABoxes representing the full descriptions of clearings of elegant models.

Definition 10. Let K := (A, T ) be a ZOIQ-KB in Scott's normal form. A K-summary S is any ⊆-minimal ABox satisfying, for all names a,b ∈ ind(K), all the conditions below.

• (I) S contains either a ≈ b or ¬(a ≈ b).
• (II) For all concept names A appearing in K we have that S contains either A(a) or ¬A(a).
• (III) For all NFA A from K, and all concept names A from C(ind(T ), A) ∪ C⇝(A), S contains A(a) or ¬A(a).
• (IV) For all role names r appearing in K we have that S contains either r(a,b) or ¬r(a,b).
• (V) For all NFA A from K, and all role names r from R(ind(T ),A), the ABox S contains r(a,b) or ¬r(a,b).
• (VI) For all number restrictions (≥n r).⊤ from K, and for all o ∈ ind(T ), there are thresholds t a cl , t a ch , and t a o in {=m,≥n+1 | 0 ≤ m ≤ n} for which S contains Clrngr t a cl (a), Chldr t a ch (a), and Desr ,o t a o (a).
• (VII) Root(a) ∈ S and edge(a,b) ∈ S.

In the case when only a ZOIQ-TBox T is given, we define T -ghost-summaries as ({ ≈ }, T )-summaries. ◀

Invoking the previously-established bounds on the number and sizes of concepts and roles occurring in decorations (i.e. the ones stated at the end of Definitions 3, 4, and 7), we infer:

Lemma 14. Let Kand T be, respectively, aZOIQ-KB and a ZOIQ-TBox, both in Scott's normal form. We have that every K-summary is of size polynomial in |K|. Moreover, there are exponentially (in |T |) many T -ghost-summaries and each of them is of size polynomial w.r.t. |T |. ◀

While a K-summary can be easily extracted from the clearing of any elegant model of K, the converse direction requires two extra assumptions, dubbed clearing- and subtree-consistency.

7 Consistent Summaries

The notion of clearing-consistency ensures that a given summary S is a good candidate for the clearing of some elegant model of K, namely (i) S does not violate "local" constraints fromK, (ii) S is virtually decorated for decorations involving number restrictions and automata, and that (iii) every element from S virtually satisfies all concepts involving automata or number restrictions from K. Below, IS denotes the minimal interpretation that corresponds to and satisfies the ABox S.

Definition 11. Let K := (A, T ) be a ZOIQ-KB in Scott's normal form, and let S be a K-summary. Let Tloc be the TBox composed of all GCIs from T except for the ones concerning NFAs and number restrictions. We say that S is clearingconsistent if IS satisfies (A, Tloc), and:

• For all GCIs A ≡ ∃Aq,q′ .⊤ from T : (i) IS is virtually (ind(T ), A)-decorated, and (ii) for all a ∈ ind(K), A(a) ∈ S iff a virtually satisfies ∃Aq,q′ .⊤ in IS .
• For all GCIs A ≡ (≥n r).⊤ from T : (i) IS is virtually (ind(T ),≥n r)-decorated, and (ii) for all a ∈ ind(K), we have that A(a) ∈ S iff a virtually satisfies (≥n r ).⊤ in IS . ◀

Based on Lemma 9 and Lemma 12 we can conclude that deciding clearing consistency can be done in PTIME.

Lemma 15. For K and S as in Def. 11 we can decide in time polynomial w.r.t. |K| · |S| whether S is clearing consistent.◀

The second required notion is the subtree-consistency. To decide whether a given summary S extends to a model of K, we need to check, for all elements d of S, the existence of a suitable forest satisfying (a relativised) K and fulfilling all the premises given by the decorations of d. This is achieved by crafting a suitable ZOIQ-KB and testing whether it has a quasi-forest model of a suitably bounded branching. To make such a KB dependent only on the TBox, we are going to use the ghost variable in place of the intended element d.

Definition 12. Let T be a ZOIQ-TBox in Scott's normal form and S be a T -ghost-summary. S is T -subtree-consistent if the ZOIQ-KBKS, := (S, Tloc∪Taut∪Tcnt) is quasi-forest satisfiable, where Tloc is as in Definition 11 and:

• Taut consists of { } ⊑ comdsc(ind(T ),A) and A ≡ rel(ind(T ), Aq,q′ ) for all GCIs A ≡ ∃Aq,q′ .⊤ from T .
• Tcnt consists of the GCIs ¬Root ⊓ A ≡ ¬Root ⊓ (≥n r ).⊤ as well as { } ⊑ desc (Chldr t ch ⊓ ⊔ o∈ind(T ) Desr ,o to ) , for the unique concepts Chldr t ch , Desr,o to satisfied by in IS, for all GCIs A ≡ (≥n r ).⊤ appearing in T . ◀

The crucial property concerning the notion of T -subtreeconsistency as well as the set ST of all T -subtree-consistent T -ghost-summaries is provided next. Its proof relies on the bounds on the concepts from Lemma 5, Lemma 6, and Definition 7, as well as the exponential time algorithm for deciding quasi-forest-satisfiability of ZOIQ-KBs from Lemma 2.

Lemma 16. For a ZOIQ-TBox T in Scott's normal form, one can decide in time exponential w.r.t. |T | if a given T - ghost-summary is T -subtree-consistent. Moreover, the set ST of all T -subtree-consistent T -ghost-summaries has size exponential in |T | and is computable in time exponential in |T |. ◀

We now lift the definition of subtree-consistency from ghost summaries to arbitrary K-summaries by producing a ghost summary per each individual name a mentioned in K. The idea is simple: we first restrict S to nominals and the selected namea, and then replaceawith the ghost variable (we must be a bit more careful if a is itself a nominal). This produces a ghost summary, for which the notion of subtree-consistency is already well-defined. The main benefit of testing subtreeconsistency of such a summary is that this guarantees the existence of a quasi-forest containing a subtree rooted at that we can afterwards "plug in" to a in S in order to produce a full model of K from S. This is formalised next.

Definition 13. Let T and ST be as in Lemma 16. For a ZOIQ-KB K := (A, T ) and a K-summary S we say that S is consistent if S is clearing-consistent and for every name a ∈ ind(K) the (T , S,a)-ghost-summary Sa belongs to ST . Sa is defined as the sum of (i) S restricted to ind(T ), (ii) S restricted to ind(T ) ∪ {a} with all occurrences of a replaced with , and (iii) {a≈ , ≈a} in case a ∈ ind(T ). ◀

It can be readily verified that all K-summaries constructed from elegant models of ZOIQ-KBs K := (A, T ) are consistent. For the opposite direction, we define a suitable notion of a merge in order to "combine" a clearing-consistent summary S with relevant subtrees provided by the subtree-consistency of (T , S,a)-ghost-summaries for all a ∈ ind(K). The interpretation constructed in this way becomes an elegant model of K.

Lemma 17. A ZOIQ-KB in Scott's normal form is quasiforest satisfiable iff there exists a consistent K-summary. ◀

8 Deciding Existence of Quasi-Forest Models

Based on Lemma 17 and all the other lemmas presented in the previous section, we can finally design an algorithm for deciding whether an input ZOIQ-KB is quasi-forest satisfiable.

Algorithm 1: Quasi-Forest Satisfiability in ZOIQ

• Input: A ZOIQ-KB K := (A, T ). Output: True iff K is quasi-forest satisfiable. 1 Turn T into Scott's normal form. // L. 13. 2 Compute the set ST . // L. 16. 3 Guess a K-summary S. // L. 14. 4 Return False if S is clearing-consistent. // L. 15. 5 Foreach a ∈ ind(K) do compute the (T , S,a)-ghost-summary Sa and return False if Sa ̸∈ ST . 6 Return True.

Lemma 18. Algorithm 1 returns True if and only if the input ZOIQ-KB K has an elegant model. Moreover, there exist polynomial function p and an exponential function e for which Algorithm 1 can be implemented with a nondeterministic Turing machine of running time bounded, for every input K := (A, T ), by e(|T |) +p(|K|) +p(|K|) · e(|T |). ◀

Suppose now that a TBox T is fixed and only an ABoxA is given as the input. Then the first two steps of Algorithm 1 are independent from the input. The same holds for the verification of whether a given ghost summary belongs to the pre-computed set ST . The desired algorithm is given below.

Algorithm 2: Deciding Quasi-Forest Satisfiability in ZOIQ w.r.t. Data Complexity

Input: An ABox A.

Parameters: ZOIQ-TBox T already in Scott's normal form and a pre-computed set ST .

Output: True iff K := (A, T ) is quasi-forest sat.

• 1 Guess a K-summary S. // NP in |K|, L. 14.
• 2 Return False if S is clearing-consistent.

// PTIME w.r.t. |K|·|S| by L. 15.

• 3 Foreach a ∈ ind(K) do compute the (T , S,a)-ghost-summary Sa and return False if Sa ̸∈ ST .

// PTIME w.r.t. |K| · (|K|+|ST |)

• 4 Return True.

We employ Lemma 18, and based on Algorithm 2 we get:

Theorem 1. For every ZOIQ-TBox T , there is an NP procedure (parametrised by T ) that for an input ABox A decides if the ZOIQ-KB K := (A, T ) is quasi-forest satisfiable. ◀

Recall that the maximal decidable fragments of ZOIQ have the elegant model property (Lemma 13). We conclude:

Theorem 2. The satisfiability problem for ZIQ, ZOQ, and ZOI is NP-complete w.r.t. the data complexity. ◀

For expressive logics from the SR family, the logical core of OWL2, it is known [Calvanese et al., 2009, Prop. 5.1] that any TBox in SRIQ, SROQ or SROI can be rewritten into ZIQ, ZOQ or ZOI. Hence, we reprove the following result:

Corollary 1. The satisfiability problem for SRIQ, SROQ, and SROI is NP-complete w.r.t. the data complexity. ◀

9 Application: Entailment of Rooted Queries

We adapt Algorithm 1 to derive coNEXPTIME-completeness of the entailment problem of (unions of) rooted conjunctive queries over ZIQ-KBs, generalising previous results on SHIQ [Lutz, 2008b, Thm. 2]. We focus on the dual problem: "Given a (union of) rooted CQs q and ZIQ-KB K := (A, T ), is there a model of K that violates q?" and show its NEXPTIME-completeness. As we work with ZIQ, by Lemma 13 we can assume that the input KB K is in Scott's normal form, and the intended model I violating q is elegant (in particular, is N-bounded for an N exponential in |T |). The crucial observation is that whenever q matches I, all the elements from the image of a match are at the depth at most |q| (as q has at least one individual name and is connected).

Hence, it suffices to construct an "initial segment" of I of depth at most |q| and degree at most N, and check if (i) q does not match it, and (ii) it can be extended to the full model of K.

Definition 14. Let R, C, D ∈ N. An (R,C,D)-forest F is a prefix-closed set of non-empty words from ZR·(ZC)+ of length at most D (Zn denotes the set of integers modulo n). The number R indicates the total number of roots of F, C denotes the maximal number of children per each element, and D indicates the maximal depth.

Treating F as a set of individual names, we define an (F,K)-initial segment of a ZOIQ-KB K as any summary S of K ∪ {a ̸≈ b | a, b ∈ F, a ̸= b} such that:

• For every a ∈ ind(K) there is b ∈ F ∩ N with a ≈ b in S, and for every b ∈ F ∩ N there is a ∈ ind(K) with a ≈ b in S.
• ((=0 child).⊤) (a) for all a ∈ F that are not leaves of F.
• ¬r(a, b) for all role names r appearing in K and all a ̸= b from F such that a is not a child of b in F (or vice-versa). ◀

The above conditions are needed to represent a forest F inside the clearing of the intended models of S. The first item of Definition 14 guarantees the proper behaviour of roots. The second item guarantees that the children of elements in the initial segment are precisely the ones that are explicitly mentioned there. Finally, the last item ensures that the "treelikeness" of the initial segment is not violated.

Lemma 19. Let K := (A, T ) be a ZIQ-KB in Scott's normal form and let q := ∨i qi be a union of rooted CQs. We have that K ̸|= q if and only if there is an (F,K)-initial segment S such that (i) F is an (R,C,D)-forest for an R bounded by |ind(K)|, C exponential in |T |, and D bounded by |q|, (ii) (S, T ) is quasi-forest satisfiable, and (iii) IS ̸|= q. ◀

Note that the forest F described above is exponential w.r.t. |K|, and thus the initial segment S can be "guessed" in NEXP.

Algorithm 3: Rooted Query Entailment in ZIQ

Input: A ZIQ-KB K := (A, T ) and a union q := ∨ni=1 qi of rooted conjunctive queries.

Output: True if and only if K ̸|= q.

• 1 Turn T into Scott's normal form.
• 2 Guess (F, K)-initial segment S of K as in Lemma 19.
• 3 Foreach 1 ≤ i ≤ n return False if IS |= qi.
• 4 Use Algorithm 1 to verify that (S, T ) is quasi-forest satisfiable and return True if this is indeed the case.

Lemma 20. Algorithm 3 returns True if and only if the input ZOIQ-KB K does not entail the input query q. Moreover, Algorithm 3 can can be implemented with a nondeterministic Turing machine of running time bounded by some function bounded exponentially w.r.t. |q| and |K|. ◀

Based on Lemma 20 we can conclude:

Theorem 3. The entailment problem for unions of rooted CQs over ZIQ-KBs is coNEXPTIME-complete. ◀

The coNEXPTIME-hardness of rooted entailment holds already for ALCI [Lutz, 2008a, Thm. 1]. Interestingly enough, we establish [Appendix L] a novel lower bound for ALCSelf.

Theorem4. The rooted conjunctive query entailment problem is coNEXPTIME-hard for ALCSelf (thus also for ZIQ). ◀

Acknowledgements

This work was supported by the ERC Grant No. 771779 (DeciGUT). Full version of this paper is available on ArXiV.