A Horn extension of DL-Lite with NL data complexity Janos Arpasi1 , Bartosz Jan Bednarczyk1,2 and Magdalena Ortiz1 1 2
Institute of Logic and Computation, TU Wien Computer Science Department, University of Wrocław
Abstract
The literature on ontology-mediated query answering (OMQA) has been shaped by two key results: first-order rewritability for DL-Lite, and PTime-hardness of data complexity for essentially every description logic beyond it. This has effectively positioned DL-Lite as the only practical choice for query rewriting, restricting OMQA solutions to first-order queries and ontologies that can be rewritten into them. This AC0 vs. PTime dichotomy is especially limiting if we consider that OMQA targets graph-structured data, and that standard graph query languages (including the recent ISO standards GQL and SQL/PGQ) are typically NL-complete. Towards identifying a rich Horn DL that can be rewritten into graph query languages and that can still express many ℰℒℐ and DL-Lite ontologies, we introduce a stratification mechanism for ℰℒℐ that controls the interaction between conjunction and recursion. In this way, we obtain ℰℒℐ ⊥ ⪯ , a description logic that strictly extends the core DL-Lite, supports reachability axioms and restricted conjunction, and allows for reasoning in NL. We establish the NL upper bound via a rewriting into nested two-way regular path queries, a fragment of GQL, providing initial evidence that our ontology language is a promising candidate for extending OMQA to graph query languages.
Keywords
complexity, query rewriting, data complexity, lightweight description logics
1. Introduction One of the seminal results in the field of Ontology-Mediated Query Answering (OMQA) is the AC0 data complexity of 𝒟ℒlite , which facilitates pure query rewritings into First-Order Logic queries [1]. Specifically, given an ontology-mediated query (𝑞, 𝒯 ), where 𝑞 is a conjunctive query and 𝒯 is a 𝒟ℒlite TBox, one can derive an FO-query 𝑞𝒯 (specifically, a union of conjunctive queries) such that the answers to 𝑞𝒯 and (𝑞, 𝒯 ) coincide over any ABox 𝒜. This result effectively reduces ontology-mediated query evaluation to the evaluation of standard database queries, bypassing the need for specialised reasoning engines at runtime. Equally influential is the observation that 𝒟ℒlite is essentially the only major family of description logics (DLs) admitting such FO-rewritings [2]. Even relatively inexpressive logics, such as ℰℒ, are PTime-complete in data complexity [2]. Consequently, they cannot be rewritten into FO, nor into any query language with subpolynomial evaluation complexity. This delineates a long-standing barrier that has shaped much of the research landscape in OMQA for the past two decades. However, this barrier may have been accepted too readily. There is a range of graph query languages that can express fundamental graph features such as reachability and path navigation, surpassing the expressive power of FO while maintaining data complexity in NL [3]. These languages have matured significantly over the past decade, culminating in the standardisation of GQL and its SQL-inspired counterpart, SQL/PGQ, in 2023 [4]. These languages are obvious candidates for OMQA, making it a true graph data access paradigm and opening up the possibility of finally moving beyond DL-Lite and FO-rewritability. The foundations of ontology-mediated queries based on graph query language— specifically, conjunctive regular path queries (CRPQs) and their variants— were laid over a decade ago, and the landscape of their computational complexity was almost fully charted [5, 6, 7, 8]. Yet these results never led to the attempted adoption of ontology-mediated graph queries in practical systems. Furthermore, none of the mentioned works addressed the fundamental tension between the limited DL 2026: 39th International Workshop on Description Logics, July 17–19, 2026, Lisbon, Portugal $ [email protected] (J. Arpasi); [email protected] (B. J. Bednarczyk); [email protected] (M. Ortiz) https://bartoszjanbednarczyk.github.io (B. J. Bednarczyk) 0000-0002-8267-7554 (B. J. Bednarczyk); 0000-0002-2344-9658 (M. Ortiz) © 2026 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
expressivity of 𝒟ℒlite and the loss of rewritability in more expressive settings. Recent advances in graph query languages offer new momentum to overcome this impasse. Finally, state-of-the-art graph query engines (like Neo4j and its query language Cypher [9]) are moving towards full support of the navigational core of GQL and SQL/PGQ,1 which supports all the extensions of CRPQs considered so far in the OMQA literature, including nested 2-way conjunctive regular path queries (N2RPQs), their most expressive variant [10]. We now see a promising path towards the ultimate goal of designing useful, expressive yet practicable ontology-mediated graph query languages that allow us to leverage existing ontologies in the OWL profiles and to pair them with the flexible navigational features of graph query languages. In this paper, we address a specific aspect of this goal that has been shamefully disregarded in the literature, namely the identification of Horn DLs that strictly extend 𝒟ℒlite and admit rewritings into graph query languages. Largely discouraged by the early negative results—like the mentioned PTimehardness of plain ℰℒ, and the same lower bound for any DL supporting qualified existential restrictions in the left-hand side of axioms and inverse roles [2]—hardly any research effort has been invested into cutting out meaningful description logics that admit rewritings into CRPQs and their extensions. To our knowledge, there are only two partial exceptions. Harmless linear ℰℒℋℐ [11] disallows the use of concept conjunction in the left-hand side of axioms, essentially restricting ℰℒℋℐ to axioms of the forms A ⊑ B, A ⊑ ∃s.B and ∃s.A ⊑ B, with s a possibly inverse role, and imposing an additional harmlessness constraint that restricts the interaction of inverses and qualified existential restrictions to keep the complexity in NL. The resulting description logic admits rewriting of atomic queries into a simple class of CRPQs, but the lack of conjunction makes it very limited as a Horn DL. Motivated by the central role of conjunction in many real-world ontologies, quasi-linear ℰℒℋℐ takes a slightly different approach, enabling restricted use of conjunction at the expense of additional restrictions on the use of inverse roles[12]. The resulting ontology language appears to be useful in practice, but it is not a proper extension of 𝒟ℒlite . We aim to push the boundary of description logics that admit reasoning in NL and rewritings into graph query languages, extending 𝒟ℒlite without compromising too much of the additional expressiveness of ℰℒℐ. In particular, instead of disallowing the use of the conjunction, we leverage the expressiveness of N2RPQs to support it in a controlled way. In this paper, we propose ℰℒℐ ⊥ ⪯ as the first NL-data-complete ontology language that fully subsumes 𝒟ℒlite and that supports conjunction and reachability axioms of the form ∃r .A ⊑ A. To maintain NL data complexity, ℰℒℐ ⊥ ⪯ utilises a stratification of concept names that guarantees a bound on the alternation induced by the interaction of reachability, inverses, and conjunction, preventing the complexity from escalating to PTime. We demonstrate NL-membership for instance checking via a rewriting into N2RPQs. Finally, we show that while the data complexity is low, the combined complexity of ℰℒℐ ⊥ ⪯ is PSpace-complete; this is consistent in spirit with the restriction of ExpTime logics to linear recursion [13], and witnesses the additional expressive power of our fragment in comparison to 𝒟ℒlite , ℰℒ, and harmless linear ℰℒℋℐ, all of which allow for reasoning in polynomial time.
2. Preliminaries We start by recalling the basics on description logics (DLs) [14] and query answering [15]. DLs. We fix countably infinite pairwise disjoint sets of individual names NI , concept names NC , and role names NR and introduce the description logic ℰℒℐ ⊥ . Starting from NC and NR , the set Cℰℒℐ ⊥ of ℰℒℐ ⊥ -concepts is built using the following concept constructors: conjunction (C ⊓ D), existential restriction (∃r .C) and bottom and top concepts (⊥, ⊤), with the following grammar: C, D ::= ⊥ | ⊤ | A | C ⊓ D | ∃r .C | ∃r̄ .C,
1
https://neo4j.com/docs/cypher-manual/current/appendix/gql-conformance/
where C, D are Cℰℒℐℋ⊥ -concepts, A ∈ NC is a concept name, r ∈ NR is a role name, and r̄ denotes its inverse. We will always assume that the inverse of r̄ is just r , and use (possibly decorated) letters s to denote possibly inverted roles. KBs. Assertions take the form C(a), s(a, b) for a, b ∈ NI , C ∈ NC ∪ {⊤, ⊥} and (possibly inverted) role s. A general concept inclusion (GCI) has the form C ⊑ D for concepts C, D. We employ C ≡ D as a shorthand for the two GCIs C ⊑ D and D ⊑ C. A knowledge base (KB) 𝒦 := (𝒜, 𝒯 ) is composed of a finite non-empty set 𝒜 (ABox) of assertions and a finite non-empty set 𝒯 (TBox) of GCIs. The elements of 𝒜 ∪ 𝒯 are called axioms. Let ind(𝒦), con(𝒦), rol(𝒦) denote the sets of all individual, concept, and role names from 𝒦, respectively (including ⊤, ⊥ in con(𝒦) and role inverses in rol(𝒦)). We use the analogue notation for TBoxes and ABoxes as well. A KB 𝒦 is in normal form if all its GCIs conform to the following pattern: A ⊑ B,
A ⊓ B ⊑ C,
A ⊑ ∃s.B,
∃s.A ⊑ B,
where A, B, C are either concept names, ⊤, or ⊥, while s is a possibly inverted role. Without loss of generality, we also require that ⊤ and ⊥ do not appear in GCIs of the form A ⊓ B ⊑ C, and that trivially unsatisfiable formulae like ∃s.⊥ are always replaced with ⊥. Table 1 Concepts and roles in ℰℒℐ ⊥ . Name
Syntax Semantics
bottom concept ⊥ top concept ⊤ concept name A role name r inverse role r̄ conc. negation ¬C conc. intersection C ⊓ D exist. restriction ∃s.C
∅ Δℐ Aℐ ⊆ Δℐ r ℐ ⊆ Δℐ ×Δℐ {(e, d) | (d, e) ∈ r ℐ } Δℐ ∖ C ℐ C ℐ ∩ Dℐ {d | ∃e.(d, e) ∈ s ℐ ∧ e ∈ Cℐ }
Table 2 Axioms in ℰℒℐ ⊥ . Axiom 𝛼
ℐ |= 𝛼, if
C⊑D
Cℐ ⊆ Dℐ
C(a) r (a, b)
ℐ
TBox 𝒯
ℐ
a ∈C ABox 𝒜 (aℐ , bℐ ) ∈ r ℐ
The semantics of ℰℒℐ ⊥ is defined via interpretations ℐ := (Δℐ , ·ℐ ) composed of a non-empty set Δℐ called the domain of ℐ and an interpretation function ·ℐ mapping individual names to elements of Δℐ , concept names to subsets of Δℐ , and role names to subsets of Δℐ × Δℐ . This mapping is extended to complex concepts (see Table 1) and finally used to define satisfaction of assertions and GCIs (see Table 2). Structures are interpretations with a partial assignment of individual names. We say that an interpretation ℐ satisfies a KB 𝒦 := (𝒜, 𝒯 ) (or ℐ is a model of 𝒦, written: ℐ |= 𝒦) if it satisfies all axioms of 𝒜 ∪ 𝒯 . A KB is consistent (or satisfiable) if it has a model and inconsistent (or unsatisfiable) otherwise. Automata and paths. By a nondeterministic automaton (NFA) A we understand, as usual, a tuple (𝑄, Σ, 𝛿, 𝑞0 , 𝐹 ) where 𝑄 is a finite set of states, Σ is a finite alphabet, 𝛿 ⊆ 𝑄 × Σ × 𝑄 is the transition relation, 𝑞0 ∈ 𝑄 is the initial state and 𝐹 ⊆ 𝑄 is the set of accepting states. All NFA considered in this paper are over finite subsets of {r , r̄ , C? | r ∈ NR , C ∈ NC }, where the expressions of the form C? are called tests. For a natural number 𝑛 we also define 𝑛-nested NFA (nNFA) by induction: a 0NFA is just an NFA, and an (𝑛+1)NFA is an NFA whose alphabet may contain letters A? for A being an nNFA. By a run of an NFA A = (𝑄, Σ, 𝛿, 𝑞0 , 𝐹 ) over an interpretation ℐ, we understand a finite sequence of tuples (d0 , 𝑞0 , 𝑤1 , 𝑞1 , d1 ), . . . , (dℓ−1 , 𝑞ℓ−1 , 𝑤ℓ , 𝑞ℓ , dℓ ) in Δℐ × 𝛿 × Δℐ such that for all 𝑖 < ℓ we have: (i) if 𝑤𝑖+1 = r , then (d𝑖 , d𝑖+1 ) ∈ r ℐ , (ii) if 𝑤𝑖+1 = r̄ , then (d𝑖+1 , d𝑖 ) ∈ r ℐ , and (iii) if 𝑤𝑖+1 = C? for a concept name C, then d𝑖 = d𝑖+1 and d𝑖 ∈ Cℐ .
A run is accepting if 𝑞ℓ ∈ 𝐹 . We say that a run starts from d if d0 = d. We define runs of an 𝑛NFA for all 𝑛 > 0 analogously, adding the following extra condition: (iv) if 𝑤𝑖+1 = B? for an (𝑛−1)NFA B, then d𝑖 = d𝑖+1 and there is an accepting run of B starting from d𝑖 . Queries. An instance query (IQ) 𝑞 is an expression of the form C(a), where a is an individual name and C is a concept name. An interpretation ℐ satisfies such a query (written ℐ |= 𝑞) if aℐ ∈ Cℐ . A nested two-way regular path query (N2RPQ) 𝑞 is an expression of the form ∃𝑥A(a, 𝑥) for an individual name a and an nNFA A. An interpretation ℐ satisfies such a query (written ℐ |= 𝑞) if there is an accepting run of A in ℐ starting from aℐ . In the query entailment problem, we are given a KB 𝒦 := (𝒜, 𝒯 ) and a query 𝑞 and ask if 𝒦 |= 𝑞, i.e. whether every model of 𝒦 satisfies 𝑞. Here we are interested in computational complexity of this problem. If all of 𝒜, 𝒯 and 𝑞 are part of the input, we talk about combined complexity. If only 𝒜 is part of the input, while 𝒯 and 𝑞 are fixed beforehand, we talk about data complexity. Given a query language ℒ (say, first-order logic or N2RPQ) say that a TBox 𝒯 is ℒ-rewritable if for every instance query 𝑞 there is a query 𝑞 ′ in ℒ such that for all ABoxes 𝒜 and all a ∈ ind(𝒜), we have (𝒜, 𝒯 ) |= 𝑞(a) if and only if 𝒜 |= 𝑞 ′ (a). Briefly speaking, the query entailment problem over KBs with ℒ-rewritable TBoxes boils down to just evaluating ℒ-queries over ABoxes.
3. Our Logic and the Rewriting In this section, we introduce ℰℒℐ ⊥ ⪯ and present the rewriting of instance queries into N2RPQs. Definition 3.1. We say that a KB 𝒦 = (𝒜, 𝒯 ) in normal form is stratified whenever there exists a preorder ⪯ on con(𝒦) ∪ rol(𝒦) satisfying all the following conditions (where ≺ denotes the strict part of ⪯, and A, B, C are concept names, and D stands for a concept name or ⊤): • Whenever (A ⊑ B) ∈ 𝒯 , then A ⪯ B. • Whenever (A ⊓ B ⊑ C) ∈ 𝒯 , then A ⪯ C, B ⪯ C, and at least one of A ≺ C or B ≺ C holds. • Whenever (A ⊑ ∃s.D) ∈ 𝒯 , then A ⪯ D or D = ⊤; and A ⪯ s. • Whenever (∃s.D ⊑ B) ∈ 𝒯 , then either D ≺ B, D = B, or D = ⊤; and s ⪯ D. • We assume that r ⪯ r − and r − ⪯ r for all role names r . ⊥ By ℰℒℐ ⊥ ⪯ we denote the fragment of ℰℒℐℋ whose KBs are in normal form and stratified.
◀
Note that the above conditions on ⪯ do not apply to GCIs with ⊥ on the right-hand side, and ⊥ hence disjointness of concepts is not subject to any restriction in ℰℒℐ ⊥ ⪯ . It is easy to see that ℰℒℐ ⪯ strictly extends 𝒟ℒlite [14, Def. 7.9] while being a strict fragment of ℰℒℐℋ⊥ . A separating example is the non-first-order-rewritable TBox 𝒯 := {∃r .A ⊑ A}, which belongs to our logic but not to 𝒟ℒlite [14, Consequence of Thm. 7.8]. On the other hand, 𝒯 ′ := {∃r .A ⊓ ∃s.A ⊑ A} is a TBox that ′ belongs to ℰℒℐ ⊥ but not to ℰℒℐ ⊥ ⪯ . The rewritings of the instance query A(𝑥) over both 𝒯 and 𝒯 are inherently recursive and thus fall outside first-order logic. A reader familiar with Datalog [14, Sec. 7.3] will recognize that the rewriting for 𝒯 fits into the fragment of Datalog with linear recursion, whereas the one for 𝒯 ′ does not. Consequently, the rewriting of 𝒯 ′ into nested automata or well-known graph query languages such as GQL is not possible, while the rewriting of 𝒯 can be expressed as a regular path query, e.g. as (r * ; A?)(a, 𝑥). Requiring recursion to be linear is a crucial condition for guaranteeing the existence of rewritings of instance queries. In our approach, this is enforced by the preorder ⪯ in Definition 3.1 (in particular by the second condition).
Example 3.2. It is a well-known fact that in expressive DLs such as ℰℒℐ, one can simulate concept conjunction by means of role inverses. Indeed, the GCI A ⊓ B ⊑ C can be replaced by the following set of GCIs 𝒯 := {A ⊑ ∃r .⊤, ∃r̄ .B ⊑ D, ∃r .D ⊑ C}, where the role r and the concept name D are fresh. We stress that reusing this “conjunction emulation” approach for arbitrary concepts fails in our logic due to the presence of the built-in order ⪯. Indeed, it is routine to check that, in the presence of ⪯, the following facts hold for 𝒯 : A ⪯ r , r ⪯ B, B ≺ D, r ⪯ C, D ≺ C. In particular, this implies A ≺ C and B ≺ C, and thus A and B cannot be arbitrary concepts. ◀ The main technical contribution of this paper is the rewriting of instance queries under ℰℒℐ ⊥ ⪯ontologies into nested two-way regular path queries. We state the result formally below. ′ Theorem 3.3. Take a ℰℒℐ ⊥ ⪯ -TBox 𝒯 and an instance query 𝑞. We can compute an N2RPQ 𝑞 such that for all ABoxes 𝒜 and all a ∈ ind(𝒜), we have (𝒜, 𝒯 ) |= 𝑞(a) if and only if 𝒜 |= 𝑞 ′ (a). ◀
In the remainder of the section, we fix 𝑞 and 𝒯 as in the statement of Theorem 3.3, and present how to construct the desired query 𝑞 ′ .2 Soundness and completeness of the rewriting are established in the next two sections, respectively. Our construction of 𝑞 ′ is inductive and based on the height of the concept/role names 𝛼 in 𝒯 , namely the length of the longest chain of concept or role names 𝛼1 ≺ 𝛼2 ≺ . . . ≺ 𝛼𝑛 for which 𝛼𝑛 = 𝛼. This notion is lifted to concepts from 𝒯 as follows: the height of ⊤ and ⊥ is 0, and the height of concepts of the form ∃s.A is the maximum of heights of s and A. For convenience, let 𝒯 ⇂𝑛 and 𝒜⇂𝑛 respectively denote the set of GCIs and assertions from 𝒯 and 𝒜 that solely concepts of height at most 𝑛. Our inductive claim is stated below (𝒯 ⇂−1 is just the empty set). Inductive assumption for 𝑛 ∈ N: For each concept name A in 𝒯 of height 𝑛, we can construct an 𝑛-nested NFA AA over {B? | B ∈ con(𝒯 ⇂𝑛 )} ∪ rol(𝒯 ⇂𝑛 ) ∪ {AB ? | B ∈ con(𝒯 ⇂𝑛−1 )} such that for all ABoxes 𝒜 and all a ∈ ind(𝒜), we have (𝒜, 𝒯 ) |= A(a) if and only if 𝒜 |= ∃𝑥AA (a, 𝑥). Less formally, our goal is to construct an automaton that witnesses the satisfaction of A at a given node in an ABox, using the GCIs in 𝒯 as inference rules. Its alphabet consists of (possibly inverted) role names, tests over concept names of height at most 𝑛 (enabling the automaton to read labels from the ABox), and inductively constructed automaton-tests detecting membership in concepts of height strictly less than 𝑛 (enabling it to delegate the verification of certain concepts to “simpler” automata). The states are pairs (premise, goal ), where the first component is a set of concept names from 𝒯 and the second one is a single one of those. Along a run, the automaton tracks the concepts from 𝒯 already known to hold at the current node (the premise), as well as those that remain to be verified there (the goal). Transitions are either derived from the GCIs in 𝒯 , mimicking a (reversed) entailment proof via successive rule applications, or read off from the ABox, recording which concept names hold at the current node. For instance, whenever a GCI A ⊑ B is present in 𝒯 and B belongs to the goal, the automaton may replace B in its goal with A. Finally, a state is accepting if and only if its goal component is empty, i.e. all required concepts have been verified; in other words, a run is accepting if the automaton successfully discharges all its goals. Base case. We handle the base case first, as it already captures the key challenges of our technique. For the reader’s convenience, we interweave formal definitions with informal descriptions. Definition 3.4. Fix a concept name A ∈ con(𝒯 ⇂0 ). We define an NFA AA := (𝑄, Σ, 𝛿, 𝑞0 , 𝐹 ) as follows. • We set Σ := {B? | B ∈ con(𝒯 ⇂0 )} ∪ rol(𝒯 ⇂0 ), as already stated in the inductive claim. Note that in the base case no automaton-tests are used. • The state set 𝑄 consists of all pairs (premise, goal ) for premise ⊆ con(𝒯 ⇂0 ) and goal ∈ con(𝒯 ⇂0 ). • The initial state is 𝑞0 := ({⊤}, A). The intuition is straightforward: we wish to verify A at the current node, but we currently only know that ⊤ holds there. 2
W.l.o.g. we assume that the concept name from 𝑞 occur in 𝒯 ; otherwise the entailment is trivially false.
• The set of accepting states 𝐹 consists of all pairs in 𝑄 where goal ∈ premise or ⊥ ∈ premise. • The transition relation 𝛿 is defined as the minimal subset of 𝑄 × Σ × 𝑄 such that, for every state 𝑞 := (premise, goal ), all the following conditions hold. (weak) For any subset premise ′ of premise, there is a transition from 𝑞 to (premise ′ ∪ {⊤}, goal ) labelled “⊤?”. This allows the automaton to forget some of the information in the premise, which will be crucial for handling GCIs with conjunctions in the premise. (data) For any concept name B ∈ con(𝒯 ⇂0 ), there is a transition from 𝑞 to (premise ∪ {B}, goal ) labelled “B?”. This allows the automaton to read from the ABox which concept names hold at the current node and add them to the premise. (sbus) For any GCI C ⊑ D from 𝒯 ⇂0 , if goal = D, there exists a transition from 𝑞 to (premise, C) labelled “⊤?”. This formalizes the following backward reasoning: to prove D given the GCI C ⊑ D, it suffices to prove C. (succ) If goal = D, then for any GCI ∃s.C ⊑ D in 𝒯 ⇂0 , there is a transition from 𝑞 to ({⊤}, C) labelled “s”. This formalizes the following reasoning: given the GCI ∃r .C ⊑ D, the automaton may move to a neighbouring node in the ABox and verify that C holds there. The premise is reset to {⊤} since the automaton does not have any non-trivial information on that neighbour. The fact that it suffices to track a single successor at a time—which is essential for the feasibility of our construction—follows from the linear recursion enforced by Definition 3.1. (anon) For any concepts B and D from con(𝒯 ⇂0 ), if the KB ({C(a) | C ∈ premise ∪ {B}}, 𝒯 ⇂0 ) entails D(a) and goal = D, there is a transition from 𝑞 to (premise, B) labelled “⊤?”. Though this transition may appear redundant, it is crucial for correctness: it enables the automaton to infer the existence of anonymous individuals satisfying certain concepts, which is essential for handling GCIs with existential restrictions in the premise. Note that GCIs of the form A ⊓ B ⊑ C play no role in the definition of 𝛿 here. By the second condition of Definition 3.1 and by the definition of a normal form, such GCIs cannot solely involve concepts from con(𝒯 ⇂0 ). ◀ We illustrate our construction of AA for a (non-first-order-rewritable) TBox 𝒯 := {∃r .A ⊑ A} and an instance query 𝑞 := A(a). The relevant fragment of AA is depicted below. It is equivalent to the regular path query (r * ; A?)(a, 𝑥), the expected rewriting for this query and TBox.
start 𝑟, ⊤?
{⊤}, {A}
A?
{⊤, A}, {A}
A?, ⊤?
Inductive step. We now proceed with the inductive step. The main difference with the base case is that we can now also use automaton-tests in the transitions to deal with GCIs involving conjunction. Definition 3.5. Fix 𝑛 > 0 and a concept name A ∈ con(𝒯 ⇂𝑛 ), and assume that AB has already been defined for each B ∈ con(𝒯 ⇂𝑛−1 ). We define a nested NFA AA := (𝑄, Σ, 𝛿, 𝑞0 , 𝐹 ) as follows. • The components Σ, 𝑄, 𝑞0 , and 𝐹 are defined as in the base case, with the sole difference that Σ now also contains automaton-tests of the form AB ? for each B ∈ con(𝒯 ⇂𝑛−1 ), and all occurrences of 𝒯 ⇂0 are replaced with 𝒯 ⇂𝑛 . • The transition relation 𝛿 is the minimal subset of 𝑄 × Σ × 𝑄 such that, for every state 𝑞 := (premise, goal ), all conditions from the base case (after replacing 𝒯 ⇂0 with 𝒯 ⇂𝑛 ) hold, as well as the following three conditions are satisfied.
(noc) For any GCI B ⊓ C ⊑ D in 𝒯 ⇂𝑛 with B ∈ premise and goal = D, there exists a transition from 𝑞 to (premise, C) labelled “⊤?”. The case of the GCI B ⊓ C ⊑ D with C ∈ premise and D ∈ goal is handled analogously. This formalises the standard backward reasoning step for conjunction. (aut) For any concept name B ∈ con(𝒯 ⇂𝑛−1 ) there is a transition from 𝑞 to (premise ∪ {B}, goal ) labelled “AB ?”. As the height of B is strictly less than that of A, the automaton can “delegate” the proof of B to the nested automaton AB (well-defined by the inductive hypothesis). ◀
4. Soundness In this section we establish the “only if” direction of Theorem 3.3, restated for convenience below. Lemma 4.1. Let 𝒯 be a stratified ℰℒℐ ⊥ ⪯ -TBox, A(𝑎) be an instance query, and AA be an nNFA from Definition 3.5. Then for all for all ABoxes 𝒜 we have that 𝒜 |= ∃𝑥AA (a, 𝑥) implies (𝒜, 𝒯 ) |= A(a). ◀ Proof. Fix a TBox 𝒯 . The proof is by induction on the height 𝑛 of the concept name 𝐴. We assume that for all 𝑛′ < 𝑛 and concept names B ∈ con(𝒯 ⇂𝑛′ ), the statement of Lemma 4.1 holds for the instance query B(a). Then we consider an instance query A(a) with A ∈ con(𝒯 ⇂𝑛 ). Fix an ABox 𝒜, a model ℐ of (𝒜, 𝒯 ), and let 𝜌 = 𝜌1 · · · 𝜌ℓ be an accepting run of AA in ℐ starting from aℐ , which exists by entailment 𝒜 |= ∃𝑥AA (a, 𝑥)). For convenience, let 𝜌𝑖 unfold to (d𝑖−1 , 𝛿𝑖 , d𝑖 ) with 𝑞𝑖 = (premise 𝑖 , goal 𝑖 ) and 𝛿𝑖 = (𝑞𝑖−1 , 𝑤𝑖 , 𝑞𝑖 ). In the appendix, we prove the following claim. The proof is by induction on 𝑖, backwards from 𝑖 = ℓ to 𝑖 = 0. If d𝑖 satisfies all concepts from premise 𝑖 in ℐ, then it also satisfies all concepts from goal 𝑖 . From this claim, the statement of the lemma follows, as the initial state of AA is ({⊤}, A), while the accepting states have their goal already proven.
5. Completeness The goal of this section is to establish the remaining direction of Theorem 3.3. But before we can proceed with the proof, we need some additional definitions. First, we recall the standard notion of a derivation. Definition 5.1. Let 𝒯 be an ℰℒℐ ⊥ ⪯ -TBox. A 𝒯 -derivation of A(a) from an ABox 𝒜 is a finite sequence 𝒜0 , 𝒜1 , . . . , 𝒜𝑛 of ABoxes such that 𝒜0 is a subset of 𝒜, 𝒜𝑛 contains A(a), and for every 𝑖 < 𝑛 the ABox 𝒜𝑖+1 can be derived from 𝒜𝑖 (denoted 𝒜𝑖 ⇝𝒯 𝒜𝑖+1 ), i.e. there exists a GCI B ⊑ C in 𝒯 and an individual name b such that:3 • Both B and C are concept names or ⊤, B(b) ∈ 𝒜𝑖 , and 𝒜𝑖+1 = 𝒜𝑖 ∪ {C(b)}; • B is of the form B1 ⊓ B2 , both B1 (b) and B2 (b) belong to 𝒜𝑖 , and 𝒜𝑖+1 = 𝒜𝑖 ∪ {C(b)}; • B is a concept name or ⊤, C is of the form ∃s.C1 , B(b) ∈ 𝒜𝑖 , and 𝒜𝑖+1 = 𝒜𝑖 ∪ {s(b, c), C1 (c)} for some fresh individual name c; • B is of the form ∃s.B1 , both s(b, c) and B1 (c) belong to 𝒜𝑖 , and 𝒜𝑖+1 = 𝒜𝑖 ∪ {C(b)}; or • ⊥(b) ∈ 𝒜𝑖 , and 𝒜𝑖+1 = {A(a)}. In all of these cases, if B(b) is (one of) the mentioned concept assertions in 𝒜𝑖 and A(a) is the newly added concept assertion to 𝒜𝑖+1 , we say that B(b) was used to infer A(a). We call the number 𝑛 the length of the derivation. We say that A(a) is 𝒯 -derivable from 𝒜 whenever there exists a 𝒯 -derivation of A(a) from 𝒜. ◀ 3
For brevity, we abuse the notation and write ⊤(b) ∈ 𝒜𝑖 to indicate that b appears in 𝒜𝑖 .
The following example illustrates the notion of derivations and will be continued later. Example 5.2. Consider an ABox 𝒜ex := {A(a)}, an ℰℒℐ ⊥ ⪯ -TBox 𝒯ex := {A ⊑ B, A ⊓ B ⊑ C, C ⊑ ∃r .⊤, ∃r .⊤ ⊑ D}, and an atomic query 𝑞ex := D(a). We enumerate the GCIs of 𝒯ex in order of appearance as 𝛼0 , . . . , 𝛼3 . The reader may easily verify that the sequence 𝒜0 , . . . , 𝒜4 is a 𝒯ex -derivation of 𝑞ex from 𝒜ex , where 𝒜0 = 𝒜, 𝒜1 = 𝒜0 ∪ {B(a)}, 𝒜2 = 𝒜1 ∪ {C(a)}, 𝒜3 = 𝒜2 ∪ {r (a, b), ⊤(b)}, and 𝒜4 = 𝒜3 ∪ {D(a)}. In particular, for all 𝑖 < 4 we have 𝒜𝑖 ⇝{𝛼𝑖 } 𝒜𝑖+1 . ◀ The following lemma links derivations with entailment. Its proof is standard, and hence we omit it. Lemma 5.3 (folklore). Let 𝒜 be an ABox, 𝒯 be a stratified ℰℒℐ ⊥ ⪯ -TBox, and A(a) be an instance query. Then (𝒜, 𝒯 ) |= A(a) if and only if A(a) can be 𝒯 -derived from 𝒜. ◀ Our built-in stratification can also be reflected in the derivations, leading to the following notion. Definition 5.4. Let 𝒯 , 𝒜, and A(a) be as in Definition 5.1, and suppose that A is of height ℓ. A (𝒯 , ℓ)derivation of A(a) from 𝒜 is a finite sequence (𝒜0 , A0 (a0 )), (𝒜1 , A1 (a1 )), . . ., (𝒜𝑛 , A𝑛 (a𝑛 )) of ABoxes and instance queries (called active queries) with concepts from con(𝒯 ⇂ℓ ) such that: • A𝑛 (a𝑛 ) = A(a), for all 𝑖 ≤ 𝑛, the sequence 𝒜0 , . . . , 𝒜𝑖 is a 𝒯 ⇂ℓ -derivation of A𝑖 (a𝑖 ) from 𝒜, and • for all 𝑖 < 𝑛: if 𝒜𝑖 ⇝{C⊑D} 𝒜𝑖+1 for some GCI C ⊑ D from 𝒯 ⇂ℓ with D of height ℓ, then 1. if B′ is a concept name of height ℓ and occurs in C, then A𝑖 (a𝑖 ) = B′ (a𝑖 ); 2. A𝑖+1 (a𝑖+1 ) = B′′ (a𝑖+1 ) for the concept name B′′ that occurs in D.
◀
The following example illustrates the notion of stratified derivation. Example 5.5. Let 𝒜ex , 𝒯ex , and 𝑞ex be as in Example 5.2. Suppose that the heights of A, B, C, r , D are 0, 1, 2, 2, and 3, respectively. The reader may verify that the sequence (𝒜0 , A0 (a0 )), . . . , (𝒜4 , A4 (a0 )) is a (𝒯ex , 3)-derivation of 𝑞ex from 𝒜ex , where A0 (a0 ) = A(a), A1 (a1 ) = B(a), A2 (a2 ) = C(a), A3 (a3 ) = ⊤(b), and A4 (a4 ) = D(a). ◀ With the next lemma, we connect stratified derivations with the entailment of instance queries. Lemma 5.6. Let 𝒯 be an ℰℒℐ ⊥ ⪯ -TBox, 𝒜 be an ABox, and A(a) be an instance query such that (𝒜, 𝒯 ) |= A(a). Then there exists a (𝒯 , ℓ)-derivation of A(a) from 𝒜 with ℓ being the height of A. ◀ Proof Sketch. Our proof proceeds by induction and our inductive statement is: For every 𝑑, for every ℓ, and every instance query A(a) with concept A of height ℓ for which there exists a derivation of (𝒜, 𝒯 ) |= A(a) of length 𝑑, there also exists a (𝒯 , ℓ)-derivation of A(a) from 𝒜. For the case 𝑑 = 0 it suffices to take the pair (𝒜, A(a)) as the desired (𝒯 , ℓ)-derivation of A(a) from 𝒜. For the induction step we can perform a case distinction based on the GCI that was used in the last step of the derivation. We provide a detailed execution of this argument in the appendix. We next establish an important property of “stratified” derivations. Lemma 5.7. Let 𝒯 be an ℰℒℐ ⊥ ⪯ -TBox, 𝒜 be an ABox, and let (𝒜0 , A0 (a0 )), (𝒜1 , A1 (a1 )), . . ., (𝒜𝑛 , A𝑛 (a𝑛 )) be a (𝒯 , ℓ)-derivation of some concept A(a) from 𝒜. For all 𝑖 ≥ 0, if a𝑖 ∈ ind(𝒜) and a𝑖−1 ̸∈ ind(𝒜), such that A𝑖−1 (a𝑖−1 ) was used to infer A𝑖 (a𝑖 ), then: 𝑖 • if there is no 𝑗 < 𝑖 with a𝑗 = a𝑖 , then (𝒯 ⇂ℓ , 𝒜𝑖−1⇂aℓ−1 ) |= A𝑖 (a𝑖 ); and 𝑖 • otherwise for some 𝑗 < 𝑖 with a𝑗 = a𝑖 we have (𝒯 ⇂ℓ , 𝒜𝑖−1⇂aℓ−1 ∪ {A𝑗 (a𝑖 )}) |= A𝑖 (a𝑖 ),
where 𝒜𝑖⇂aℓ−1 is the restriction of 𝒜𝑖 to assertions about a concerning concepts of height at most ℓ − 1. ◀
Informally, in this lemma we claim, that in the described setting, A𝑖 (a𝑖 ) can be inferred solely by considering the already known facts about a𝑖 of some lower height, together with the TBox restricted to lower levels, and, if it exists as an active query, a single concept assertion on a𝑖 of height ℓ. Proof. Without loss of generality, assume that 𝒜 contains ⊤(a) for all a ∈ ind(𝒜). Consider the directed implication graph of 𝒜𝑖 (denoted 𝒢𝒜𝑖 ), whose vertices are the concept assertions in 𝒜𝑖 . There is a directed edge from B(b) to C(c) if there exists 𝑗 < 𝑖 such that B(b) ∈ / 𝒜𝑗 , C(c) ∈ 𝒜𝑗 , and C(c) was used to derive B(b) and add it to 𝒜𝑗+1 . By Definition 5.1, if such an edge exists, then either b = c or s(b, c) ∈ 𝒜𝑗+1 . Inspecting Definition 5.1, we observe that no derivation step creates edges between existing individuals. Hence, along any path in 𝒢𝒜𝑖 from an “anonymous” individual c ∈ / ind(𝒜) connected to a𝑖 (i.e., s(a𝑖 , c) ∈ 𝒜𝑖 ) to a “named” individual b ∈ ind(𝒜), the first named individual encountered is a𝑖 . Thus every maximal path 𝜌 in 𝒢𝒜𝑖 starting at A𝑖 (a𝑖 ) and proceeding to A𝑖−1 (a𝑖−1 ), must have some 𝑘 > 2 such that 𝜌𝑘 = C(a𝑖 ) for some C, since the last vertex of 𝜌 lies in 𝒜. Furthermore, at most one such maximal path starting at A𝑖 (a𝑖 ) can contain a vertex A𝑗 (a𝑖 ) of height ℓ. Otherwise, suppose two paths 𝜌 and 𝜌′ exist. Then they coincide up to some 𝜌𝑘 = 𝜌′𝑘 = B(b), but diverge at the next step. By the definition of the implication graph, this implies that B(b) was derived using a rule C ⊓ D ⊑ B, with b = c = d. Then one of C, D must have strictly lower height, contradicting stratification if a later vertex of height ℓ reappears on the diverging path. Since only active queries can have height ℓ, the assertion A𝑗 (a𝑖 ) must have been active at some stage prior to 𝑖. All other assertions about a𝑖 on paths from A𝑖 (a𝑖 ) have lower height and thus already occur in 𝒜𝑖−1 . It remains to derive 𝑖 A𝑖 (a𝑖 ) from (𝒯 ⇂ℓ , 𝒜𝑖−1⇂aℓ−1 ∪ {A𝑗 (a𝑖 )}). If no such A𝑗 (a𝑖 ) occurs, we take A𝑗 (a𝑖 ) = ⊤(a𝑖 ). Let 𝑆 be the set of assertions in 𝒢𝒜𝑖 reachable from A𝑖 (a𝑖 ) without passing through assertions about a𝑖 . Let 𝑠 = (𝑠1 , . . . , 𝑠|𝑆| ) enumerate 𝑆 in the order of first occurrence in the derivation. Define: 𝑖 ∪ {A𝑗 (a𝑖 )}, 𝒜′0 = 𝒜𝑖−1⇂aℓ−1
𝒜′𝑘+1 = 𝒜′𝑘 ∪ {𝑠𝑘+1 } ∪ {r (b, c) | b, c ∈ ind(𝒜′𝑘 ∪ {𝑠𝑘+1 }), r (b, c) ∈ 𝒜𝑖 }. We claim this yields a valid derivation of A𝑖 (a𝑖 ). First, 𝑠 is a reverse topological ordering of 𝑆: if (B(b), C(c)) is an edge, then C(c) was derived before B(b), hence appears earlier in 𝑠. Now consider 𝑠𝑘+1 = B(b) derived via D ⊑ E. For any predecessor C(c) of B(b), we have C(c) ∈ 𝑆 or c = a𝑖 . In the latter case, C(a𝑖 ) is either A𝑗 (a𝑖 ) or already in 𝒜′0 . By the ordering of 𝑠, all such C(c) belong to 𝒜′𝑘 . If D ⊑ E does not involve existential restrictions, it applies directly. If it is of the form ∃r .C ⊑ B, then all required role assertions are present in 𝒜′𝑘 by construction. If it is of the form C ⊑ ∃r .B, then b is introduced as a fresh individual, and 𝒜′𝑘+1 correctly reflects this extension. Thus, each step is valid, completing the derivation. We can now demonstrate how to retrieve accepting runs of the nested automata from the stratified derivations guaranteed by the entailment of instance queries. In this way, we can finally establish the remaining direction of Theorem 3.3, restated below for convenience. Lemma 5.8. Let 𝒯 be a stratified ℰℒℐ ⊥ ⪯ -TBox, A(a) be an instance query with A of height 𝑛, and AA be the 𝑛-nested NFA for A constructed in Definition 3.5. Then for all ABoxes 𝒜 we have that (𝒜, 𝒯 ) |= A(a) implies 𝒜 |= ∃𝑥 AA (a, 𝑥), i.e. there exists a accepting run of AA starting from aℐ . ◀ Proof Sketch. Fix 𝒯 and 𝒜 as in the statement of the lemma, and let ℐ |= (𝒯 , 𝒜). We proceed by induction over the length 𝑑 of the run. More specifically, we prove the following inductive claim: For all 𝑑 ∈ N, all ℓ ∈ N, all a ∈ ind(𝒜), and all concept names A ∈ con(𝒯 ⇂ℓ ), whenever there is a (𝒯 , ℓ)-derivation of A(a) from 𝒜 of length 𝑑, then there is an accepting run of AA starting from aℐ . The base case is immediate. Indeed, take any ℓ and A ∈ con(𝒯 ⇂ℓ ), and suppose that there is a (𝒯 , ℓ)-derivation of A(a) from 𝒜 of length 𝑑. Then such a derivation has the form (𝒜0 , A(a)) for some 𝒜0 ⊆ 𝒜 with A(a) ∈ 𝒜0 . Thus, to construct an accepting run of AA we can step from 𝑞0 :=
({⊤}, A) to 𝑞1 := ({A, ⊤}, A), via a (data)-transition, which is already a final state. More formally, (aℐ , 𝑞0 , A?, 𝑞1 , aℐ ) is the desired run of AA starting from aℐ . For the inductive step, we again do a case distinction on the last step of the (𝒯 , ℓ)-derivation to simulate that derivation step in the automaton. In particular “reasoning in the anonymous part” is possible thanks to Lemma 5.7. In the appendix we provide a full version of this argument. The following example illustrates the proof above. Example 5.9. Let 𝒜ex , 𝒯ex , and 𝑞ex be as in Example 5.2, and let (𝒜0 , A0 (a0 )), . . . , (𝒜4 , A4 (a0 )) be the (𝒯ex , 3)-derivation of 𝑞ex from 𝒜ex from Example 5.5. Fix a model ℐ |= (𝒯ex , 𝒜ex ). By inspecting the proof of Lemma 5.8, we see that the following run (aℐ , 𝛿0 , aℐ ), . . . , (aℐ , 𝛿4 , aℐ ) of AD starting from aℐ is produced, where: • 𝛿0 = (({⊤}, D), ⊤?, ({⊤}, C)) corresponds to the use of a (anon)-transition parametrised by C, invoking the anonymous part of ℐ. • 𝛿1 = (({⊤}, C), A?, ({⊤, A}, C)) corresponds to the use of a (data)-transition reading A(a) from the ABox. • 𝛿2 = (({⊤, A}, C), ⊤?, ({⊤, A}, B)) corresponds to the use of a (noc)-transition invoking the GCI A ⊓ B ⊑ C. • 𝛿3 = (({⊤, A}, B), ⊤?, ({⊤, A}, A)) corresponds to the use of a (sbus)-transition invoking the GCI A ⊑ B. This puts the automaton in an accepting state. ◀ We have proved that our rewriting of instance queries under ℰℒℐ ⊥ ⪯ -ontologies into N2RPQs is sound and complete. As evaluating N2RPQs is feasible in NL [16], we obtain the desired complexity result. Corollary 5.10. Take a fixed ℰℒℐ ⊥ ⪯ -TBox 𝒯 and an instance query 𝑞. For every ABox 𝒜, deciding (𝒜, 𝒯 ) |= 𝑞(a) is feasible in NL.
6. Combined Complexity We conclude the paper by establishing PSpace-completeness of instance query entailment in ℰℒℐ ⊥ ⪯. Lower bound. We reduce from QBF, which is PSpace-hard even for prenex 3-DNF formulas [17, Thm. 6.1]. The reduction ⋁︀ already works for linear orders ⪯. Consider 𝜙 = 𝑄1 𝑥1 · · · 𝑄𝑛 𝑥𝑛 𝜓, where 𝑄𝑖 ∈ {∃, ∀} and 𝜓 = 𝑚 𝑗=1 𝜆𝑗1 ∧ 𝜆𝑗2 ∧ 𝜆𝑗3 , where 𝜆s are literals. We define a singleton ABox 𝒜, a 𝒯 , True and a concept C0 such that C0 holds for the only individual in 𝒜 if and only if 𝜙 is valid. We employ the following concept and role names {L𝑖 , X0𝑖 , X1𝑖 , CTrue , CTrue,0 , CTrue,1 | 0 ≤ 𝑖 ≤ 𝑛} ∪ {A1𝑗 , A2𝑗 | 1 ≤ 𝑗 ≤ 𝑚} 𝑖 𝑖 𝑖
{r0,𝑖 , r1,𝑖 | 0 ≤ 𝑖 ≤ 𝑛}.
Intended models are binary trees of depth 𝑛 rooted at a, where level 𝑖 (marked by L𝑖 ) encodes the value of 𝑥𝑖 via X0𝑖 or X1𝑖 . Parent-to-child connections on level 𝑖 are realised by roles r𝑑,𝑖 (where 𝑑 ∈ {0, 1} denotes a direction). The concepts CTrue propagate truth of the suffix formula, and A1𝑗 , A2𝑗 simulate 𝑖 conjunctions of literals. Let 𝒜 = {L0 (a)} and query CTrue 0 (a). The TBox 𝒯 is defined as: 𝒯 := {L𝑖 ⊑ ∃r0,𝑖+1 .L𝑖+1 , L𝑖 ⊑ ∃r1,𝑖+1 .L𝑖+1 | 𝑖 ∈ {0, . . . , 𝑛 − 1}}
(1)
∪ {∃r 0,𝑖+1 .L𝑖 ⊑ X0𝑖+1 , ∃r 1,𝑖+1 .L𝑖 ⊑ X1𝑖+1 | 𝑖 ∈ {0, . . . , 𝑛 − 1}}
(2)
∪ {∃r 𝑑,𝑖 .X0𝑖 ⊑ X0𝑖 , ∃r 𝑑,𝑖 .X1𝑖 ⊑ X1𝑖 | 𝑖 ∈ {1, . . . , 𝑛}, 𝑑 ∈ {0, 1}} ∪ {L𝑛 ⊓ X1𝑖 ⊑ A1𝑗 | 𝜆𝑗1 = 𝑥𝑖 , 𝑗 ∈ {1, . . . , 𝑚}, 𝑖 ∈ {1, . . . , 𝑛}} ∪ {L𝑛 ⊓ X0𝑖 ⊑ A1𝑗 | 𝜆𝑗1 = ¬𝑥𝑖 , 𝑗 ∈ {1, . . . , 𝑚}, 𝑖 ∈ {1, . . . , 𝑛}}
(3) (4) (5)
∪ {A1𝑗 ⊓ X1𝑖 ⊑ A2𝑗 | 𝜆𝑗2 = 𝑥𝑖 , 𝑗 ∈ {1, . . . , 𝑚}, 𝑖 ∈ {1, . . . , 𝑛}}
(6)
∪ {A1𝑗 ⊓ X0𝑖 ⊑ A2𝑗 | 𝜆𝑗2 = ¬𝑥𝑖 , 𝑗 ∈ {1, . . . , 𝑚}, 𝑖 ∈ {1, . . . , 𝑛}} ∪ {A2𝑗 ⊓ X1𝑖 ⊑ CTrue | 𝜆𝑗3 = 𝑥𝑖 , 𝑗 ∈ {1, . . . , 𝑚}, 𝑖 ∈ {1, . . . , 𝑛}} 𝑛 2 0 True ∪ {A𝑗 ⊓ X𝑖 ⊑ C𝑛 | 𝜆𝑗3 = ¬𝑥𝑖 , 𝑗 ∈ {1, . . . , 𝑚}, 𝑖 ∈ {1, . . . , 𝑛}} True,0 True,1 ∪ {∃𝑟0 .CTrue , ∃𝑟1 .CTrue | 𝑖 ∈ {0, . . . , 𝑛 − 1}} 𝑖+1 ⊑ C𝑖 𝑖+1 ⊑ C𝑖 True,0 True,1 True True ∪ {C𝑖 ⊑ C𝑖 , C𝑖 ⊑ C𝑖 | 𝑖 ∈ {0, . . . , 𝑛 − 1}, 𝑄𝑖+1 = ∃} ∪ {CTrue,0 ⊓ CTrue,1 ⊑ CTrue | 𝑖 ∈ {0, . . . , 𝑛 − 1}, 𝑄𝑖+1 = ∀} 𝑖 𝑖 𝑖
(7) (8) (9) (10) (11) (12)
Finally, we can order our subset of NC ∪ NR with ⪯ as follows: L0 ≺ r0,1 ≺ r1,1 ≺ X01 ≺ X11 ≺ L1 ≺ r0,2 ≺ r1,2 ≺ X02 ≺ X12 ≺ . . . L𝑛 ≺ A11 ≺ A21 ≺ A12 ≺ A22 ≺ . . . A1𝑚 ≺ A2𝑚 ≺ True,0 True,1 True CTrue ≺ CTrue,0 ≺ CTrue,1 ≺ CTrue 𝑛 𝑛 𝑛 𝑛−1 ≺ C𝑛−1 ≺ C𝑛−1 ≺ . . . ≺ C0
The proof of the following lemma is standard. Check the appendix for details. ⊥ Lemma 6.1. (𝒜, 𝒯 ) |= CTrue 0 (a) if and only if 𝜙 is valid. Hence, instance query entailment in ℰℒℐ ⪯ is PSpace-hard (in combined complexity). ◀
Upper bound. Let 𝒜 be an input ABox, 𝒯 an ℰℒℐ ⊥ ⪯ -TBox, and 𝑞 := A(a) an instance query. By Theorem 3.3, to decide whether (𝒯 , 𝒜) |= 𝑞, it suffices to construct the nNFA A given by the rewriting and check for an accepting run of A on 𝒜 starting at a. The size of A is exponential in |𝒯 | (due to subsets of concepts in the premise component of states), so it cannot be materialised explicitly. Instead, we construct it on the fly during evaluation. Any accepting run has length bounded by the number of states of A, hence exponential in |𝒯 |. Such a bound can be tracked using an exponentially large counter encoded in polynomial space. The procedure guesses a run of A on 𝒜 from a step by step, incrementing the counter and verifying the correctness of each transition. If an accepting state is reached within the bound, we accept; otherwise, we reject. Since only the current state and the counter need to be stored, the procedure runs in polynomial space. Thus, instance query entailment in ℰℒℐ ⊥ ⪯ is in PSpace (in combined complexity). The only subtle point is the verification of transitions. While most transitions of A can be checked directly using the ABox and the current state, Steps (anon) and (aut) require additional care. For (aut) transitions, observe that the automaton test AB ? involves only concepts of strictly lower height than A. Thus, by an inductive construction over heights and by the use of PSpace oracles, this step can be fully implemented in polynomial space. For (anon) transitions, which correspond to classical ⊥ reasoning in ℰℒℐ ⊥ ⪯ , we adapt the standard alternating polynomial-space algorithm for ℰℒℐℋ . The key observation is that the number of alternations is bounded by the height of the input concept. By the classical result that alternating PSpace with polynomially many alternations coincides with PSpace [18, Thm. 4.2], this step is also feasible in polynomial space. A more detailed exposition will be given in revised version of the paper. We thus conclude: Theorem 6.2. Instance query entailment in ℰℒℐ ⊥ ⪯ is PSpace-complete (in combined complexity).
◀
7. Conclusions and Future Work ⊥ In this work, we introduced ℰℒℐ ⊥ ⪯ , a novel fragment of ℰℒℐℋ that extends 𝒟ℒlite and is based on the idea of “stratified conjunction.” By means of a suitable rewriting into nested two-way regular path queries (N2RPQs), we established that the instance query entailment problem for our logic is NL-complete with respect to data complexity. Our future and ongoing work will pursue several directions. First, we plan to incorporate role hierarchies into our logic, which should be achievable with only minor modifications to our approach.
Second, we aim to move beyond instance queries and investigate the combined complexity of query answering for ℰℒℐ ⊥ ⪯ with respect to the full class of nested C2RPQs. We are optimistic that this can be achieved through a suitable adaptation of the techniques presented by Bienvenu et al. [6]. Third, we intend to provide support for concrete domains. To do so, we plan to combine the query rewriting approach of Baader et al. [19] with the recent model of C2RPQs with data values introduced by Figueira et al. [20]. Finally, since the target of our rewriting is (a fragment of) GQL, we plan to investigate the practical applicability of our approach by implementing it and evaluating it on real-world datasets.
Acknowledgments This research was funded in whole by the Austrian Science Fund (FWF) 10.55776/PIN8884924.
Declaration on Generative AI During the preparation of this work, the author(s) used ChatGPT and Claude in order to: grammar and spelling check, polish the text. After using these tool(s)/service(s), the author(s) reviewed and edited the content as needed and take(s) full responsibility for the publication’s content.
References [1] D. Calvanese, G. De Giacomo, D. Lembo, M. Lenzerini, R. Rosati, Tractable reasoning and efficient query answering in description logics: The DL-Lite family, Journal of Automated Reasoning (2007). [2] D. Calvanese, G. De Giacomo, D. Lembo, M. Lenzerini, R. Rosati, Data complexity of query answering in description logics, Artificial Intelligence (2013). [3] L. Libkin, W. Martens, F. Murlak, L. Peterfreund, D. Vrgoc, Querying graph data: Where we are and where to go, in: PODS 2025, ACM, 2025. [4] N. Francis, A. Gheerbrant, P. Guagliardo, L. Libkin, V. Marsault, W. Martens, F. Murlak, L. Peterfreund, A. Rogova, D. Vrgoc, A researcher’s digest of GQL (invited talk), in: ICDT 2023, LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. [5] M. Bienvenu, M. Ortiz, M. Šimkus, Regular path queries in lightweight description logics: Complexity and algorithms, Journal of Artificial Intelligence Research (2015). [6] M. Bienvenu, D. Calvanese, M. Ortiz, M. Šimkus, Nested regular path queries in description logics, in: KR, 2014. [7] D. Calvanese, T. Eiter, M. Ortiz, Regular path queries in expressive description logics with nominals, in: IJCAI 2009, 2009. [8] M. Ortiz, S. Rudolph, M. Simkus, Query answering in the horn fragments of the description logics SHOIQ and SROIQ, in: T. Walsh (Ed.), IJCAI 2011, IJCAI/AAAI, 2011. [9] A. Gheerbrant, L. Libkin, L. Peterfreund, A. Rogova, Database theory in action: Cypher, GQL, and regular path queries, in: ICDT 2025, LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. [10] N. Francis, A. Gheerbrant, P. Guagliardo, L. Libkin, V. Marsault, W. Martens, F. Murlak, L. Peterfreund, A. Rogova, D. Vrgoc, GPC: A pattern calculus for property graphs, in: PODS 2023, ACM, 2023. [11] M. M. Dimartino, P. T. Wood, A. Calì, A. Poulovassilis, Efficient ontology-mediated query answering: Extending DL-LiteR and linear ELH, Journal of Artificial Intelligence Research (2025). [12] B. Löhnert, N. Augsten, C. Okulmus, M. Ortiz, Towards practicable algorithms for rewriting graph queries beyond DL-Lite, in: The Semantic Web, Springer Nature Switzerland, 2025. [13] E. Dantsin, T. Eiter, G. Gottlob, A. Voronkov, Complexity and expressive power of logic programming, ACM Computing Surveys (2001). [14] F. Baader, I. Horrocks, C. Lutz, U. Sattler, An Introduction to Description Logic, Cambridge University Press, 2017.
[15] M. Ortiz, M. Šimkus, Reasoning and Query Answering in Description Logics, in: Reasoning Web, 2012. [16] J. L. Reutter, M. Romero, M. Y. Vardi, Regular queries on graph databases, Theory Comput. Syst. 61 (2017). [17] T. J. Schaefer, The complexity of satisfiability problems, in: STOC, 1978. [18] A. K. Chandra, D. Kozen, L. J. Stockmeyer, Alternation, Journal of the ACM (1981). [19] F. Baader, S. Borgwardt, M. Lippmann, Query rewriting for DL-Lite with n-ary concrete domains, in: IJCAI, 2017. [20] D. Figueira, A. Jeż, A. W. Lin, Data path queries over embedded graph databases, in: PODS 2022, 2022.
A. Appendix on Soundness Here we provide the proof of Lemma 4.1, which we restate once more below. Lemma A.1. Let 𝒯 be a stratified ℰℒℐ ⊥ ⪯ -TBox, A(𝑎) be an instance query, and AA be an nNFA from Definition 3.5. Then for all for all ABoxes 𝒜 we have that 𝒜 |= ∃𝑥AA (a, 𝑥) implies (𝒜, 𝒯 ) |= A(a). ◀ Proof. Fix a TBox 𝒯 . The proof is by induction on the height 𝑛 of the concept name 𝐴 (the induction in turn contains a nested induction on the length of a run of the automaton). We assume that for all 𝑛′ < 𝑛 and concept names B ∈ con(𝒯 ⇂𝑛′ ), the statement of Lemma 4.1 holds for the instance query B(a). Let us move forward to an instance query A(a) with A ∈ con(𝒯 ⇂𝑛 ). Fix an ABox 𝒜, a model ℐ of (𝒜, 𝒯 ), and let 𝜌 = 𝜌1 · · · 𝜌ℓ be an accepting run of AA in ℐ starting from aℐ , which exists by entailment 𝒜 |= ∃𝑥AA (a, 𝑥)). For convenience, let 𝜌𝑖 unfold to (d𝑖−1 , 𝛿𝑖 , d𝑖 ) with 𝑞𝑖 = (premise 𝑖 , goal 𝑖 ) and 𝛿𝑖 = (𝑞𝑖−1 , 𝑤𝑖 , 𝑞𝑖 ). We now proceed by induction on 𝑖, backwards from 𝑖 = ℓ to 𝑖 = 0, and prove that: (†) if d𝑖 satisfies all concepts from premise 𝑖 in ℐ, then it also satisfies all concepts from goal 𝑖 in ℐ. Then the statement of the lemma follows as the initial state of AA is ({⊤}, A), while the accepting states have their goal already proven. The base case follows trivially, since goal ℓ ∈ premise or ⊥ ∈ premise. Hence, let us focus on the case when 𝑖 < ℓ and the induction hypothesis already holds for all 𝑖′ > 𝑖. Suppose d𝑖 satisfies all concepts from premise 𝑖 in ℐ. We distinguish cases depending on how the transition 𝛿𝑖 := (𝑞𝑖−1 , 𝑤𝑖 , 𝑞𝑖 ) was created in the construction of AA . • It was created by the rule (weak). After inspecting the construction, we see that: (i) premise 𝑖+1 is a subset of premise 𝑖 , (ii) goal 𝑖+1 = goal 𝑖 , (iii) 𝑤𝑖 = ⊤?, and thus (iv) d𝑖 = d𝑖+1 . As d𝑖 satisfies all concepts from premise 𝑖 , then by (iv) and (i) we have that d𝑖+1 satisfies all concepts from premise 𝑖+1 . Thus, we can invoke the inductive assumption for 𝑖 + 1 to infer that d𝑖+1 satisfies goal 𝑖+1 in ℐ. Together with (iv) and (ii), this implies that d𝑖 satisfies goal 𝑖 in ℐ, as desired. • It was created by Rule (data). After inspecting the construction, we see that: (i) goal 𝑖+1 = goal 𝑖 , and there exists a concept C for which: (ii) premise 𝑖+1 = premise 𝑖 ∪ {C}, (iii) 𝑤𝑖 = C?, and hence (iv) d𝑖 = d𝑖+1 and (v) d𝑖 ∈ Cℐ . By our assumptions together with (ii) and (v), we have that d𝑖 satisfies all concepts from premise 𝑖+1 . By (iv), we can invoke the inductive hypothesis for 𝑖 + 1 to infer that d𝑖 satisfies all concepts from goal 𝑖+1 in ℐ, which by (i) concludes the proof. • It was created by the rule (sbus). After inspecting the construction, we see that there is a GCI C ⊑ D in 𝒯 such that: (i) goal 𝑖 = D, (ii) premise 𝑖+1 = premise 𝑖 , (iii) goal 𝑖+1 = C, (iv) 𝑤𝑖 = ⊤?, and thus (v) d𝑖 = d𝑖+1 . By our assumptions together with (ii) and (v), we can invoke the inductive hypothesis for 𝑖+1 to infer that d𝑖 satisfies goal 𝑖+1 = C in ℐ. It remains to show that d𝑖 also satisfies D. This follows from the fact that d𝑖 satisfies C and ℐ is a model of 𝒯 , containing C ⊑ D. • It was created by Rule (succ). After inspecting the construction, we see that there is a GCI ∃s.C ⊑ D in 𝒯 such that: (i) goal 𝑖 = D, (ii) goal 𝑖+1 = C, (iii) premise 𝑖+1 = {⊤}, (iv) 𝑤𝑖 = s, and thus (v) (d𝑖 , d𝑖+1 ) ∈ s ℐ . We can trivially conclude that d𝑖+1 satisfies all concepts from
premise 𝑖+1 . Invoking the inductive hypothesis, we infer that d𝑖+1 also satisfies goal 𝑖+1 = C by (ii). From (v) and the fact that ℐ is a model of ∃s.C ⊑ D, we conclude that d𝑖 satisfies D, which by (i) concludes the proof. • If 𝛿𝑖 was created by Rule (anon). After inspecting the construction, we see that there are a concepts D and B from 𝒯 such that: (i) goal 𝑖+1 = B, (ii) premise 𝑖+1 = premise 𝑖 , (iii) ({C(a) | C ∈ premise 𝑖 } ∪ {B(a)}, 𝒯 ) entails D(a), (iv) 𝑤𝑖 = ⊤?, and thus (v) d𝑖 = d𝑖+1 . By our assumptions, d𝑖 satisfies all concepts from premise 𝑖 , and hence, by (iii) and ℐ |= 𝒯 , it also satisfies D, if d𝑖 satisfies B. Together with (ii) and (v), we can invoke the inductive hypothesis for 𝑖 + 1 to infer that d𝑖 satisfies all concepts from goal 𝑖+1 in ℐ, which by (i) concludes the proof. • It was created by the rule (noc). After inspecting the construction, we see that there is a GCI B ⊓ C ⊑ D in 𝒯 such that: (i) B ∈ premise 𝑖 , (ii) goal 𝑖 = D, (iii) premise 𝑖+1 = premise 𝑖 , (iv) goal 𝑖+1 = C, (v) 𝑤𝑖 = ⊤?, and thus (vi) d𝑖 = d𝑖+1 . By our assumptions together with (iii) and (vi), we can invoke the inductive hypothesis for 𝑖+1 to infer that d𝑖 satisfies goal 𝑖+1 = C in ℐ. We also know that d𝑖 satisfies B by (i). Since ℐ is a model of 𝒯 , it follows that d𝑖 satisfies D as well, which by (iv) concludes the proof. • If 𝛿𝑖 was created by Rule (aut). After inspecting the construction, we see that there is a concept B ∈ con(𝒯 ⇂𝑛−1 ) such that: (i) goal 𝑖+1 = goal 𝑖 , (ii) premise 𝑖+1 = premise 𝑖 ∪{B}, (iii) 𝑤𝑖 = AB ?, and thus (iv) d𝑖 = d𝑖+1 . It suffices to show that d𝑖 satisfies B in ℐ. Indeed, by (ii) and (iv), we can invoke the inductive hypothesis for 𝑖 + 1 to infer that d𝑖 satisfies all concepts from goal 𝑖+1 in ℐ, which by (i) concludes the proof. To see that d𝑖 satisfies B, we invoke the inductive hypothesis for 𝑖 + 1 and B (recall that B has height strictly smaller than 𝑛). As we exhausted all cases, the proof is complete.
B. Appendix on Completeness Proof of Lemma 5.6. Our proof proceeds by induction and our inductive statement is: For every 𝑑, for every ℓ, and every instance query A(a) with concept A of height ℓ for which there exists a derivation of (𝒜, 𝒯 ) |= A(a) of length 𝑑, there also exists a (𝒯 , ℓ)-derivation of A(a) from 𝒜. The case 𝑑 = 0 is immediate: it suffices to take the pair (𝒜, A(a)) as the desired (𝒯 , ℓ)-derivation of A(a) from 𝒜. We now assume 𝑑 > 0 and that the inductive hypothesis holds for all smaller values of 𝑑. Next, take any ℓ and a concept A of height ℓ, and let 𝒜0 , . . . , 𝒜𝑑 be the shortest 𝒯 -derivation of A(a) from 𝒜. Aiming to construct the desired (𝒯 , ℓ)-derivation of A(a) from 𝒜, we proceed by case distinction on the shape of the GCI B ⊑ A such that 𝒜𝑑−1 ⇝{B⊑A} 𝒜𝑑 . 1. B = ⊤ and A is a concept name. Then, exactly as in the base case, we simply take (𝒜, A(a)) as the desired derivation. 2. A and B are concept names with B ⪯ A. Observe that 𝒜0 , . . . , 𝒜𝑑−1 is a 𝒯 -derivation of B(a) from 𝒜 of length 𝑑−1. By the inductive hypothesis, there exists a (𝒯 , ℓ)-derivation (𝒜′0 , A′0 (a0 )), . . . , (𝒜′𝑘 , A′𝑘 (a𝑘 )) of B(a) from 𝒜. By design, a𝑘 = a, A′𝑘 = B, and 𝒜′0 ⊆ 𝒜. Thus (𝒜′0 , A′0 (a0 )), . . . , (𝒜′𝑘 , A′𝑘 (a)), (𝒜′𝑘 ∪ {A(a)}, A(a)) is the desired (𝒯 , ℓ)-derivation of A(a) from 𝒜. 3. A is a concept name (or A = ⊥) and B = B1 ⊓ B2 for concept names B1 ⪯ A and B2 ≺ A (and analogously for B = B2 ⊓ B1 ). Observe that 𝒜0 , . . . , 𝒜𝑑−1 is a 𝒯 -derivation of both B1 (a) and B2 (a) from 𝒜 of length 𝑑−1. By the inductive hypothesis, there exist (𝒯 , ℓ)- and (𝒯 , ℓ−1)-derivations (𝒜′0 , A′0 (a′0 )), . . . , (𝒜′𝑘 , A′𝑘 (𝑎′𝑘 )) and (𝒜′′0 , A′′0 (a′′0 )), . . . , (𝒜′′𝑚 , A′′𝑚 (a′′𝑚 )) of B1 (a) and B2 (a) from 𝒜, respectively. Note that A′𝑘 = B1 and a = a′𝑘 . One can verify that the sequence (𝒜′0 , A′0 (a′0 )), . . . , (𝒜′𝑘 , A′𝑘 (a)), (𝒜′𝑘 ∪ 𝒜′′0 , B1 (a)), . . . , (𝒜′𝑘 ∪ 𝒜′′𝑚 , B1 (a)), (𝒜′𝑘 ∪ 𝒜′′𝑚 ∪ {A(a)}, A(a)) is the desired (𝒯 , ℓ)-derivation of A(a) from 𝒜.
4. B = ⊤ and A = ∃s.⊤. We simply take (𝒜, ⊤(a)), (𝒜∪{s(a, b)}, ⊤(b)) as the desired derivation, where b is a fresh individual name. 5. B = ⊤ and A = ∃s.A′ for some concept name A′ with B ⪯ A′ . We simply take (𝒜, ⊤(a)), (𝒜 ∪ {s(a, b), A′ (b)}, A′ (b)) as the desired derivation, where b is a fresh individual name. 6. B is a concept name and A = ∃s.A′ for some concept name A′ with B ⪯ A′ . Then there is a 𝒯 derivation 𝒜0 , . . . , 𝒜𝑑−1 of A′ (a) from 𝒜 of length 𝑑−1. By the induction hypothesis there exists a (𝒯 , ℓ)-derivation (𝒜′0 , A′0 (a0 )), . . . , (𝒜′𝑘 , A′𝑘 (𝑎𝑘 )) of A′ (a) from 𝒜, where A′𝑘 = A′ = B or B ≺ A′ . In either case, we can take (𝒜′0 , A′0 (a0 )), . . . , (𝒜′𝑘 , A′𝑘 (𝑎𝑘 )), (𝒜′𝑘 ∪ {s(a, b), A′ (b)}, A′ (b)) as the desired derivation, where b is a fresh individual name. 7. A is a concept name (or A = ⊥) and B = ∃s.C for C ∈ {⊤, A} or C another concept name. Then there is a 𝒯 -derivation 𝒜0 , . . . , 𝒜𝑑−1 of C(b) from 𝒜 of length 𝑑−1 with s(a, b) ∈ 𝒜𝑑−1 . By the induction hypothesis there exists a (𝒯 , ℓ)-derivation (𝒜′0 , A′0 (a0 )), . . . , (𝒜′𝑘 , A′𝑘 (𝑎𝑘 )) of C(b) from 𝒜. By design, a𝑘 = b, A′𝑘 = C, and 𝒜′0 ⊆ 𝒜. Thus (𝒜′0 , A′0 (a0 )), . . . , (𝒜′𝑘 , A′𝑘 (a𝑘 )), (𝒜′𝑘 ∪ {A(a)}, A(a)) is the desired (𝒯 , ℓ)-derivation of A(a) from 𝒜. As we exhausted all the cases, we are done with the inductive step. This concludes the proof. We now also give a full version of the proof for Lemma 5.8 restated below. Lemma B.1. Let 𝒯 be a stratified ℰℒℐ ⊥ ⪯ -TBox, A(a) be an instance query with A of height 𝑛, and AA be the 𝑛-nested NFA for A constructed in Definition 3.5. Then for all ABoxes 𝒜 we have that (𝒜, 𝒯 ) |= A(a) implies 𝒜 |= ∃𝑥 AA (a, 𝑥), i.e. there exists a accepting run of AA starting from aℐ . ◀ Proof of Lemma 5.8. Fix 𝒯 and 𝒜 as in the statement of the lemma, and let ℐ |= (𝒯 , 𝒜). We proceed by induction over 𝑑, with the inductive claim stated below. For all 𝑑 ∈ N, all ℓ ∈ N, all a ∈ ind(𝒜), and all concept names A ∈ con(𝒯 ⇂ℓ ), whenever there is a (𝒯 , ℓ)-derivation of A(a) from 𝒜 of length 𝑑, then there is an accepting run of AA starting from aℐ . The base case is immediate. Indeed, take any ℓ and A ∈ con(𝒯 ⇂ℓ ), and suppose that there is a (𝒯 , ℓ)-derivation of A(a) from 𝒜 of length 𝑑. Then such a derivation has the form (𝒜0 , A(a)) for some 𝒜0 ⊆ 𝒜 with A(a) ∈ 𝒜0 . Thus, to construct an accepting run of AA we can step from 𝑞0 := ({⊤}, A) to 𝑞1 := ({A, ⊤}, A), via a (data)-transition, which is already a final state. More formally, (aℐ , 𝑞0 , A?, 𝑞1 , aℐ ) is the desired run of AA starting from aℐ . We now move to the inductive step, assuming that our inductive statement holds for all 𝑑′ < 𝑑. Consider any ℓ, an a, and a concept name A ∈ con(𝒯 ⇂ℓ ). Suppose that (𝒜0 , A0 (a0 )), (𝒜1 , A1 (a1 )), . . ., (𝒜𝑑 , A𝑑 (a𝑑 )) (where A𝑑 = A and a𝑑 = a) is a (𝒯 , ℓ)-derivation of A(a) from 𝒜 of length 𝑑. We perform a case analysis on the form of the GCI B ⊑ A for which 𝒜𝑑−1 ⇝{B⊑A} 𝒜𝑑 holds, in each cases pinpointing how to construct an accepting run of AA starting from aℐ . Correctness of our construction will be immediate, relying on the inductive hypothesis and the design of our automata. 1. Suppose that A is a concept name and B = ⊤. To construct an accepting run of AA we can step from 𝑞0 := ({⊤}, A) to 𝑞1 := ({⊤}, ⊤), via a (sbus)-transition, which is already a final state. Then the sequence (aℐ , 𝑞0 , ⊤?, 𝑞1 , aℐ ) is clearly a run of AA starting from aℐ . 2. Suppose A and B are concept names with B ⪯ A. Then, our derivation restricted to the first 𝑑 − 1 elements is a (𝒯 , ℓ)-derivation of B(a) from 𝒜 of length 𝑑 − 1. Hence, we can invoke the inductive hypothesis to obtain an accepting run 𝜌 := (aℐ , 𝛿1 , d2 ), . . . , (d𝑘−1 , 𝛿𝑘 , d𝑘 ) of AB starting from aℐ . Note that this is also a run of A due to B ⪯ A. Applying the (sbus)transition from ({⊤}, A) to ({⊤}, B) and then following run 𝜌 from there yields the desired run (aℐ , ({⊤}, A), ⊤?, ({⊤}, B), aℐ ), 𝜌 of AA starting from aℐ .
3. Suppose that A = ⊥ or A is a concept name with B1 ⪯ A and B2 ≺ A, for concept names B1 and B2 where we have B = B1 ⊓ B2 (the proof for B = B2 ⊓ B1 is analogous). Then, our derivation restricted to the first 𝑑 − 1 elements is also a (𝒯 , ℓ)-derivation of both B1 (a) and B2 (a) from 𝒜 of length 𝑑 − 1. Hence, we can invoke the inductive hypothesis to obtain an accepting run 𝜌1 := (aℐ , 𝛿0 , d1 ), . . . , (d𝑘−1 , 𝛿𝑘−1 , d𝑘 ) of AB1 starting from aℐ and an accepting run 𝜌2 of AB2 starting from aℐ . We construct the desired run of AA starting from aℐ as follows. We first apply an (aut)-transition from 𝑞0 := ({⊤}, A) to 𝑞1 := ({⊤, B2 }, A), followed by a (noc)-transition to reach 𝑞2 := ({⊤, B2 }, B1 ), then apply (weak) to arrive at 𝑞3 := ({⊤}, B1 ), from which we follow run 𝜌1 . Formally, the desired run of AA starting from aℐ is (aℐ , 𝑞0 , AB2 ?, 𝑞1 , aℐ ), (aℐ , 𝑞1 , ⊤?, 𝑞2 , aℐ ), (aℐ , 𝑞2 , ⊤?, 𝑞3 , aℐ ), 𝜌1 . 4. A is a concept name (or A = ⊥) and B = ∃s.C for C being either ⊤, A, or a concept name of height smaller than ℓ. Hence, there exists an individual name b such that s(a, b) ∈ 𝒜𝑑−1 and C(b) ∈ 𝒜𝑑−1 . We distinguish two cases depending on whether b is an individual name from 𝒜 or not. 4a. Suppose b ∈ ind(𝒜) (i.e. b is not anonymous); the other case will be discussed next. By the definition of a derivation, we also have s(a, b) ∈ 𝒜. Observe that our derivation restricted to the first 𝑑 − 1 elements is a (𝒯 , ℓ)-derivation of C(b) from 𝒜 of length 𝑑−1. Thus, by the inductive hypothesis, there exists an accepting run 𝜌 of AC starting from bℐ . To construct the desired run of AA , we apply a (succ)-transition from 𝑞0 := ({⊤}, A) to 𝑞1 := ({⊤}, C), stepping via s from aℐ to bℐ , from where we follow run 𝜌. Note that all transitions from 𝜌 are also transitions of AA , since C is either ⊤, A, or a concept name of height lower than that of A, and thus the same transitions are present in both automata. Finally, the desired run of AA starting from aℐ is simply (aℐ , 𝑞0 , s, 𝑞1 , bℐ ), 𝜌. 4b. Suppose b ̸∈ ind(𝒜) (i.e. b is anonymous). By the definition of a derivation, there exists a GCI D1 ⊑ ∃s.D2 that, when “applied to” aℐ , triggered the creation of bℐ (more formally: there is an index 𝑖 such that 𝒜𝑖+1 = 𝒜𝑖 ∪ {s(a, b), D2 (b)} and D1 (a) ∈ 𝒜𝑖 ). We again distinguish two cases. • There is no index 𝑗 < 𝑑 such that a = a𝑗 in the active query A𝑗 (a𝑗 ). Applying the first part of Lemma 5.7 to our derivation, we infer (𝒯 ⇂ℓ , 𝒜𝑑−1⇂aℓ−1 ) |= A𝑑−1 (a). To construct an accepting run of AA starting from aℐ , it suffices to accumulate the concept names from 𝒜𝑑−1⇂aℓ−1 into the premise (via (aut) rules, which is possible due ot the height of these concepts), followed by an (anon)-transition that simulates the classical entailment. Concretely, let E1 , E2 , . . . , E𝑚 be an enumeration of the concepts in 𝒜𝑑−1⇂aℓ−1 , and define 𝑞𝑖 := ({⊤} ∪ {E1 , . . . , E𝑖 }, A) for 0 ≤ 𝑖 ≤ 𝑚. The desired accepting run of AA starting from aℐ is then 𝜌 := 𝜌1 , . . . , 𝜌𝑚+2 , where: 𝜌𝑖 := (aℐ , 𝑞𝑖−1 , AE𝑖 ?, 𝑞𝑖 , aℐ ) for all 1 ≤ 𝑖 ≤ 𝑚, 𝜌𝑚+1 := (aℐ , 𝑞𝑚 , ⊤?, 𝑞𝑚+1 , aℐ ), where 𝑞𝑚+1 is obtained from 𝑞𝑚 by replacing its goal component with ⊤, which creates a final state. • Otherwise, let 𝑗 < 𝑑 be some index such that A𝑗 (a) is an active query. Observe that the derivation restricted to its first 𝑗 elements is a (𝒯 , ℓ)-derivation of A𝑗 (a) from 𝒜 of length less than 𝑑, so the inductive hypothesis yields an accepting run 𝜌 of AA𝑗 starting from aℐ . Moreover, we can assume without loss of generality that 𝑗 is appropriate, such that applying the second part of Lemma 5.7 to our derivation gives (𝒯 ⇂ℓ , 𝒜𝑑−1⇂aℓ−1 ∪ {A𝑗 (a)}) |= A(a). To construct an accepting run of AA starting from aℐ , it therefore suffices to accumulate the concept names from 𝒜𝑑−1⇂aℓ−1 into the premise via (aut)-rules (which is possible by the height of these concepts), then apply a (anon)-transition simulating the classical entailment and replacing the goal A with A𝑗 , then discharge all premises via a (weak)-transition, and finally follow 𝜌. Formally, let E1 , E2 , . . . , E𝑚 enumerate the concepts in 𝒜𝑑−1⇂aℓ−1 , and set 𝑞𝑖 := ({⊤} ∪ {E1 , . . . , E𝑖 }, A) for 0 ≤ 𝑖 ≤ 𝑚. The desired accepting run of AA starting from aℐ is then 𝜌′ := 𝜌′1 , . . . , 𝜌′𝑚+3 , 𝜌, where 𝜌′𝑖 := (aℐ , 𝑞𝑖−1 , AE𝑖 ?, 𝑞𝑖 , aℐ ) for 1 ≤
𝑖 ≤ 𝑚, and 𝜌′𝑚+1 := (aℐ , 𝑞𝑚 , ⊤?, 𝑞𝑚+1 , aℐ ) and 𝜌′𝑚+2 := (aℐ , 𝑞𝑚+1 , ⊤?, 𝑞𝑚+2 , aℐ ), where 𝑞𝑚+1 is obtained from 𝑞𝑚 by replacing its goal component with A𝑗 , and 𝑞𝑚+2 is obtained from 𝑞𝑚+1 by resetting its promise component to {⊤}, which gives us 𝜌′𝑚+3 := (aℐ , 𝑞𝑚+2 , ⊤?, ({⊤}, {A𝑗 }), aℐ ). As we exhausted all the cases, we are done with the inductive step. This concludes the proof.
C. Appendix on Combined Complexity In our reduction, we employ the following lemma. Lemma C.1 ([17, Theorem 6.1]). Quantified Boolean Formula (QBF), i.e. given a propositional logic formula with quantifiers, is the formula valid, is PSPACE-hard, even if the formula is in prenex-3-DNF. Lemma C.2. The following problem is PSPACE-hard (even if ⪯ is a linear ordering on the concept names): Given: An ℰℒℐ ⪯ -TBox 𝒯 , an ABox 𝒜 with a single individual name a and a concept name D Question: Does (𝒜, 𝒯 ) |= D(a) hold? Proof. Consider the formulas 𝜙, 𝜓, the ABox 𝒜, the TBox 𝒯 , the query CTrue 0 (a), the set NC of concept names, the set NR of role names, and the ordering ⪯, all as defined in the main body of the paper. We claim that (𝒜, 𝒯 ) |= CTrue 0 (a) if and only if 𝜙 ≡ True. Since making a copy per level of the roles r0 and r1 is done only to obey the ordering of the concept-/role-names, we will treat all copies of r0 and r1 , respectively, the same. We make the following observations: The universal model of (𝒜, 𝒯 ) has the form of a binary tree of depth 𝑛 with a as its root, since (1) enforces an r0 and an r1 child per node per level. Thus any node on any level 𝑖 ∈ {0, . . . , 𝑛} can be identified by one string from 𝜎 ∈ {0, 1}𝑗 by matching the r𝜎
r𝜎
r𝜎𝑗
1 2 path a −−→ ∘ −−→ · · · −−→ ∘ to the string 𝜎1 𝜎2 . . . 𝜎𝑖 ∈ {0, 1}𝑖 (the root a is identified by the empty string 𝜀). Furthermore, among the “assignment concepts” {X0𝑖 , X1𝑖 | 𝑖 ∈ {0, 1, . . . , 𝑛}}, the node 𝜎1 𝜎2 . . . 𝜎𝑖 satisfies exactly {X𝜎1 1 , X𝜎2 2 , . . . , 𝑋𝑖𝜎𝑖 }.
Claim C.3. Every node 𝜎1 . . . 𝜎𝑖 ∈ {0, 1}≤𝑛 in the universal model of (𝒜, 𝒯 ) satisfies CTrue iff. I𝜎 := 𝑖 {𝑥𝑗 ↦→ 𝜎𝑗 | 𝑗 ∈ [𝑖]} |= 𝑄𝑖+1 𝑥𝑖+1 . . . 𝑄𝑛 𝑥𝑛 𝜓(𝑥1 , . . . , 𝑥𝑖 ). Proof. We show the claim via induction on 𝑛, . . . , 0: At level 𝑛, 𝜎 := 𝜎1 . . . 𝜎𝑛 satisfies CTrue by 𝑛 definition iff. there is a monomial 𝜆𝑗1 ∧ 𝜆𝑗2 ∧ 𝜆𝑗3 s.t. 𝜎 satisfies A𝑗 and Λ𝑗1 4 , which is the case iff. 𝜎 satisfies Λ𝑗3 , Λ𝑗2 , and A1𝑗 , which is the case iff 𝜎 satisfies Λ𝑗3 , Λ𝑗2 , Λ𝑗2 , and L𝑛 (the latter one can be taken for granted). So this is the case iff I𝜎 |= 𝜓. True,𝜎𝑖+1 Assume now the claim already holds for level 𝑖 + 1, then a node 𝜎 := 𝜎1 . . . 𝜎𝑖 satisfies C𝑖 for 𝜎𝑖+1 ∈ {0, 1} iff 𝜎𝜎𝑖+1 satisfies CTrue iff I |= 𝑄 𝑥 . . . 𝑄 𝑥 𝜓(𝑥 , . . . , 𝑥 ). If 𝑄 = ∃, 𝜎𝜎 𝑖+2 𝑖+2 𝑛 𝑛 1 𝑖+1 𝑖+1 𝑖+1 𝑖+1 True,0 True,1 True then 𝜎 satisfies C𝑖 if it satisfies C𝑖 or C𝑖 and in the case of 𝑄𝑖+1 = ∀ only if it satisfies both, in either case completing the inductive step. This claim applied to the root now demonstrates our Lemma.
4
Say that a node satisfies Λ𝑗𝑘 if and only if 𝜆𝑗𝑘 = 𝑥𝑖 (respectively 𝜆𝑗𝑘 = ¬𝑥𝑖 ) and the node satisfies X1𝑖 (respectively X0𝑖 ).