Paper deep dive
A General Sufficient Condition for Rewriting Horn-ALCHI Atomic Queries into GQL
David Carral, Calixte Gruson, Quentin Manière
Intelligence
Status: not_run | Model: - | Prompt: - | Confidence: 0%
Entities (0)
Relation Signals (0)
No relation signals yet.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:The emergence of the ISO standard GQL introduces a powerful query language extending first-order logic with controlled recursion, raising the question of its applicability to evaluation of ontology-mediated queries (OMQs). We focus on OMQs consisting of atomic queries over ontologies expressed in Horn-ALCHI, an expressive Description Logic that is not, in general, first-order rewritable. To address this, we introduce DL automata, a novel formalism that captures the semantics of such OMQs via runs over fact sets. We then identify a large class of DL automata that can be rewritten into unions of conjunctive two-way regular path queries (UC2RPQs), a central fragment of GQL. Our class of automata relies on a stratification of their states, ruling out specific forms of cyclic dependencies known to raise the complexity. This yields a broad class of Horn-ALCHI OMQs that are GQL-rewritable.
Tags
Links
- Source: https://arxiv.org/abs/2608.04945v1
- Canonical: https://arxiv.org/abs/2608.04945v1
PDF not stored locally. Use the link above to view on the source site.
Full Text
126,911 characters extracted from source content.
Expand or collapse full text
11institutetext: 1LIRMM, Inria, University of Montpellier, CNRS, Montpellier, France 2DI ENS, ENS, CNRS, PSL University & Inria, France A General Sufficient Condition for Rewriting Horn-ℒℋℐHorn-ALCHI Atomic Queries into GQL David Carral Calixte Gruson and Quentin Manière Abstract The emergence of the ISO standard GQL introduces a powerful query language extending first-order logic with controlled recursion, raising the question of its applicability to evaluation of ontology-mediated queries (OMQs). We focus on OMQs consisting of atomic queries over ontologies expressed in Horn-ℒℋℐHorn-ALCHI, an expressive Description Logic that is not, in general, first-order rewritable. To address this, we introduce DL automata, a novel formalism that captures the semantics of such OMQs via runs over fact sets. We then identify a large class of DL automata that can be rewritten into unions of conjunctive two-way regular path queries (UC2RPQs), a central fragment of GQL. Our class of automata relies on a stratification of their states, ruling out specific forms of cyclic dependencies known to raise the complexity. This yields a broad class of Horn-ℒℋℐHorn-ALCHI OMQs that are GQL-rewritable. 1 Introduction In ontology-mediated query answering, user queries are enriched with conceptual knowledge about the domain of interest, described in the form of an ontology. This conceptual layer enables the use of a more user-friendly vocabulary and supports the retrieval of implicit information derived from the explicit knowledge in the ontology, thereby enriching query answers. Description Logics (DLs) are a predominant formalism for representing ontologies [3]. They provide the logical foundations of the OWL web ontology language, a W3C-standardized language for the Semantic Web [13]. In this work, we focus on the DL Horn-ℒℋℐHorn-ALCHI, an expressive language that allows the use of inverse roles and role constructors; the following example illustrates its usefulness. Example 1 Consider the set T of Horn-ℒℋℐHorn-ALCHI axioms111In the literature, DL axioms are often presented using a dedicated syntax [17]; we use equivalent first-order formulas, which are more familiar to a broader audience. given below, which formalises the notion of a Trusted user in a computer network. ∀x,y. ∀ x,y. (x,y)∧(y)→(x) Link(x,y) Sens(y)→ Sens(x) ∀x. ∀ x. (x)→∃y.(x,y)∧(y) Gate(x)→∃ y. Link(x,y) Onl(y) ∀x,y. ∀ x,y. (x,y)∧(y)→(x) Link(x,y) Onl(y)→ Onl(x) ∀x,y. ∀ x,y. (x)∧(x,y)→(y) Crit(x) Acc(x,y)→ Trust(y) ∀x. ∀ x. (x)∧(x)→(x) Sens(x) Onl(x)→ Crit(x) Furthermore, consider the fact set ℱF, defined below and illustrated in Figure˜1. \ (c1,alice),(c1,c2),(c3),(c1,c4),(c2,c3), Acc(c_1,alice), Link(c_1,c_2), Sens(c_3), Link(c_1,c_4), Link(c_2,c_3), (c4),(c5,bob),(c5,c4),(c5,c6),(c6,c7),(c7) Gate(c_4), Acc(c_5,bob), Link(c_5,c_4), Link(c_5,c_6), Link(c_6,c_7), Onl(c_7)\ The Horn-ℒℋℐHorn-ALCHI ontology ⟨,ℱ⟩ ,F entails the fact (c1) Crit(c_1): indeed, node c1c_1 has a Link path to a Sensitive node and another such path to a Gateway node (see Figure˜1); moreover, by the second axiom of T, every Gateway node has a Link to some Online node. Therefore, the ontology also entails (alice) Trust(alice). :alice [rgb]0.2734375,0.51171875,0.70703125 [named]pgfstrokecolorrgb0.2734375,0.51171875,0.70703125 Trust [rgb]0,0,0 [named]pgfstrokecolorrgb0,0,0 @color@gray@stroke0 @color@gray@fill0:alicec1:c_1: [rgb]0.2734375,0.51171875,0.70703125 [named]pgfstrokecolorrgb0.2734375,0.51171875,0.70703125 Critc2c_2c3:c_3: Sensc4:c_4: Gatebobc5c_5c6c_6c7:c_7: Onl Acc Link Link Link Acc Link Link Link Figure 1: The fact set ℱF (depicted in black), together with some of the unary facts entailed by the ontology ⟨,ℱ⟩ ,F (depicted in blue), defined in Example˜1. In the presence of DL axioms, a central reasoning task is to decide whether a given unary fact is entailed; together with the axioms, such a query forms a rule query. A common approach to evaluating a rule query over a database is to rewrite it into a classical query language, typically an FO query, while preserving equivalence, that is, ensuring that the original rule query and its rewriting are entailed by the same fact sets. This approach requires a target query language that is expressive enough to capture the ontological knowledge encoded in the axioms, but it also allows one to reuse existing database technologies, thereby avoiding the need to develop new evaluation tools. The recently released ISO standard GQL,222https://w.iso.org/standard/76120.html for graph query languages, extends the expressive power of traditional FO queries (as captured by the SQL standard) by allowing controlled forms of regular recursion. GQL can express conjunctions of two-way regular path queries and their unions (UC2RPQs), and the evaluation problem for queries at its core has been shown to be NL-complete [7, 11]. As a new standard, GQL is expected to play a central role in a wide range of applications, making it important to understand which rule queries can be rewritten into this language. Example 2 presents an equivalent rewriting into UC2RPQs, and hence into GQL, of a rule query based on Example 1. Example 2 Consider the Horn-ℒℋℐHorn-ALCHI query ⟨,(alice)⟩ , Trust(alice) , where T is the set of DL axioms described in Example˜1. This query is equivalent to the following positive conjunctive regular path query: qalice=(alice)∨∃y.[(y,alice)∧(y)]∨ q_alice TU= Trust(alice) ∃ y. [ Acc(y,alice) Crit(y) ]~ ∃y,z,w.[(y,alice)∧∗(y,z)∧(z)∧∗(y,w)∧((w)∨(w))] ~~∃ y,z,w. [ Acc(y,alice) Link^*(y,z) Sens(z) Link^*(y,w) ( Onl(w) Gate(w) ) ] That is, these two boolean queries induce the same partition over the set of all fact sets. Put differently, for any given fact set ℱ′F , the DL ontology ⟨,ℱ′⟩ ,F entails the fact (alice) Trust(alice) if and only if ℱ′F satisfies the query qaliceq_alice TU. Consequently, instead of verifying whether ⟨,ℱ′⟩ ,F entails (alice) Trust(alice) using a dedicated DL reasoner, we may simply check whether ℱ′F satisfies qaliceq_alice TU using a database management system. To conclude the example, observe that the fact set ℱF from Example˜1 satisfies qaliceq_alice TU, as expected, since ⟨,ℱ⟩ ,F does entail (alice) Trust(alice). Moreover, the rule query ⟨,(alice)⟩ , Trust(alice) is not expressible as an FO query, thereby motivating the need for rewriting techniques that go beyond this limited database query language. Contributions. We focus on rule queries with unary facts such as the one in the previous example, with rules expressed in the positive fragment of Horn-ℒℋℐHorn-ALCHI DL, defined in Section˜2. We show that these rules can be normalised into Datalog ones, in Section˜3. We then identify a large class of rule queries that can be rewritten into GQL; we proceed in two main steps. First, in Section˜4, we turn our rule queries into equivalent automata of a new form, closely related to the usual tree automata and which we refer to as DL automata. Second, in Section˜5, we identify a class of DL automata that can be rewritten into positive two-way regular path queries (PQs), and thus into UC2RPQs which in turn fall within GQL (Section˜6). Our criteria for rewritability relies on the existence of a stratification of the DL automata, which forbids some (but not all!) cyclic dependencies within its transition function. Interestingly, rule queries based upon the DL-Lite family trivially enjoy stratified automata, and thus the class we pinpoint extends DL-Lite. Additionally, our class guarantees the rewritability of rule queries that were not covered by prior attempts at rewriting into GQL [18], such as the one from Example˜2. Section˜7 elaborates further on related work; we discuss our conclusions and future work in Section˜8. This extended version of a paper to appear at ISWC 2026 contains proofs for all results in the appendix. 2 Preliminaries We assume that the reader is familiar with the syntax and semantics of first-order (FO) logic, as well as with basic notions from automata theory. Existential Rules and FO Facts. We fix pairwise disjoint, countably infinite sets Classes, Roles, Cons, and Vars of unary predicates, binary predicates, constants, and variables respectively. We often refer to unary and binary predicates as classes and roles, respectively. An inverse role is an element of =−∣∈ InvRoles=\ R^- R∈ Roles\. A role expression is an element of =∪ RoleExps= Roles∪ InvRoles. A term is an element of =∪ Terms= Cons∪ Vars. Lists of terms t1,…,tnt_1,…,t_n are written as t→ t and are often treated as sets. A class atom is a formula of the form (t) C(t) with ∈ C∈ Classes and t∈t∈ Terms. A role atom is a formula of the form (t,u) R(t,u) with ∈ R∈ Roles and t,u∈t,u∈ Terms. A FO atom is either a class atom or a role atom. Class facts, role facts, and FO facts are variable-free class atoms, role atoms, and FO atoms, respectively. For an FO formula ψ and a list x→ x of variables, we write ψ[x→]ψ[ x] to indicate that x→ x is the set of all free variables in ψ. An (existential) rule ϱ is a FO sentence of the form ∀x→,y→.(β[x→]→∃z→.η[y→,z→])∀ x, y. (β[ x]→∃ z.η[ y, z] ) where x→ x, y→ y, and z→ z are lists of variables such that (x→∪y→)∩z→=∅( x∪ y)∩ z= , and β and η are conjunctions of FO atoms with η≠∅η≠ . The rule ϱ is Datalog if z→ z is the empty list. We refer to β and ∃z→.η∃ z.η as the body and the head of ϱ , respectively. When discussing rules, we omit universal quantifiers and often identify conjunctions of atoms such as β and η above with the corresponding set. We allow rules to contain unsafe variables–universally quantified variables that appear in the head but not in the body of the rule. A knowledge base (KB) is a pair consisting of a finite rule set and a finite fact set. Description Logics. A (positive) Horn-ℒℋℐHorn-ALCHI rule is one of the following rules: 1(x)∧…∧n(x) A_1(x) … A_n(x) →(x) → B(x) 1⊓…⊓n A_1 … A_n ⊑ B (1) (x,y)∧(y) R(x,y) A(y) →(x) → B(x) ∃. ∃ R. A ⊑ B (2) (x)∧(x,y) A(x) R(x,y) →(y) → B(y) A ⊑∀. ∀ R. B (3) →(x) → B(x) ⊤ ⊑ B (4) (x) A(x) →∃y.(x,y)∧(y) →∃ y. R(x,y) B(y) A ⊑∃. ∃ R. B (5) (x,y) R(x,y) →(x,y) → S(x,y) R ⊑ S (6) (y,x) R(y,x) →(x,y) → S(x,y) − R^- ⊑ S (7) Here, A, B, and C are classes, and R and S are roles. We restrict ourselves to the positive fragment of Horn-ℒℋℐHorn-ALCHI, in which the bottom class ⊥ is not allowed; in Section˜8, we discuss how our rewriting techniques could be adapted to handle this class. We consider Horn-ℒℋℐHorn-ALCHI rules in a restricted normal form, which is without loss of generality [16]. The right-hand side shows the corresponding Description Logic syntax, included for reference only and not used further in this paper. We adopt the rule-based presentation because rules are FO logic formulas and are therefore accessible to a wider audience, and because this syntax allows us to define fact entailment for Horn-ℒℋℐHorn-ALCHI naturally via the well-known chase procedure, which we briefly present below. We consider entailment under active domain semantics as discussed later, and hence rules of type (4) are not domain-dependent. A Horn-ℒℋℐHorn-ALCHI KB is a KB whose rule set is Horn-ℒℋℐHorn-ALCHI. Query Languages. In this paper, a rule query is a pair consisting of a finite rule set and a class fact. A Datalog query is a rule query whose rule set is Datalog. A Horn-ℒℋℐHorn-ALCHI query is a rule query whose rule set is Horn-ℒℋℐHorn-ALCHI. A regular expression is an expression generated by the grammar ::=ε∣−∣(∪)∣(⋅)∣()∗, E::= R R^- ( E∪ E ) ( E· E ) ( E )^*, where ∈ R∈ Roles. For a regular expression E, let ()Lang( E) denote the set of all words over role expressions generated by E. A RE atom is a formula of the form (t,u) E(t,u) with E a regular expression and t,u∈t,u∈ Terms. A RE fact is a variable-free RE atom. A positive two-way regular path query (PQ) is a formula without occurrences of free variables generated by the grammar φ::=⊤∣(t)∣(t,u)∣(φ∧φ)∣(φ∨φ)∣∃y.φ, ::= A(t) E(t,u) ( ) ( ) ∃ y. , where (t) A(t) is a class atom, (t,u) E(t,u) is a RE atom, and y is a variable. Note that, under our definition, all PQs are Boolean queries since every occurrence of a variable in a PQ lies within the scope of an existential quantifier. Without loss of generality, we assume that every variable is quantified exactly once in a PQ. Semantics. Consider some FO sentence ψ. Given another FO sentence ψ′ψ , we write ψ⊧ψ′ψ ψ to denote entailment under under active domain semantics, that is, standard FO semantics with quantifiers ranging over the active domain. Given a finite set S of FO sentences, we write S⊧ψ ψ to denote ⋀ψ′∈Sψ′⊧ψ _ψ ∈ ψ ψ. Given a KB ⟨ℛ,ℱ⟩ ,F , we write ⟨ℛ,ℱ⟩⊧ψ ,F ψ to denote ℛ∪ℱ⊧ψR ψ. A substitution is a function mapping variables to terms. For a substitution σ and a FO formula ψ[x→]ψ[ x], let σ(ψ)σ(ψ) denote the formula obtained from ψ by replacing all occurrences of every variable x∈(σ)∩x→x (σ)∩ x with σ(x)σ(x). Consider a fact set ℱF. We define (ℱ)=−(c,d)∣(d,c)∈ℱInv(F)=\ R^-(c,d) R(d,c) \. A (possibly empty) word over role expressions … R_1… R_n is a path from a constant c to a constant d in ℱF if both c and d occur in ℱF, and there exists a list of constants e0,…,ene_0,…,e_n such that e0=ce_0=c, en=de_n=d, and (ei−1,ei)∈ℱ∪(ℱ) R_i(e_i-1,e_i) (F) for every 1≤i≤n1≤ i≤ n. In particular, for n=0n=0, the empty word ε is a path from any constant occuring in ℱF to itself. For some constants c and d occurring ℱF, we write ℱ(c,d)Paths_F(c,d) for the set of all paths from c to d in ℱF. Entailment of a PQ φ by ℱF, written ℱ⊧φF , is defined inductively as follows: • If φ=⊤ = , then ℱ⊧φF . • If φ is a class fact, then ℱ⊧φF if φ∈ℱ . • If φ is a RE fact (c,d) E(c,d), then ℱ⊧φF if ℱ(c,d)∩()≠∅Paths_F(c,d) ( E)≠ . • If φ is of the form (φ1∧φ2) ( _1 _2 ), then ℱ⊧φF if ℱ⊧φ1F _1 and ℱ⊧φ2F _2. • If φ is of the form (φ1∨φ2) ( _1 _2 ), then ℱ⊧φF if ℱ⊧φ1F _1 or ℱ⊧φ2F _2. • If φ is of the form ∃x.φ′∃ x. , then ℱ⊧φF if ℱ⊧σ(φ′)F σ( ) for some substitution σ mapping x to some constant in ℱF. Since PQs contain no free variables, defining ℱ⊧αF α for any ground atom α suffices to fully specify the semantics of entailment. For a rule query ⟨ℛ,α⟩ ,α , we write (⟨ℛ,α⟩)QM( ,α ) or (ℛ,α)QM(R,α) to refer to the set of all finite fact sets ℱF such that ⟨ℛ,ℱ⟩⊧α ,F α. For a PQ φ , let (φ)QM( ) be the set of all finite fact sets that entail φ . Here, QM stands for “query mapping”, since it associates every rule query or PQ with its semantic extension, namely the set of finite fact sets that satisfy it. A rule query or PQ γ is contained in another such query γ′γ if (γ)⊆(γ′)QM(γ) (γ ); these are equivalent if (γ)=(γ′)QM(γ)=QM(γ ). The Chase. The chase algorithm can be used to decide fact entailment and is defined here only for Datalog, since Horn-ℒℋℐHorn-ALCHI rules with existentially quantified variables can be normalised away, as explained in the following section. A trigger τ is a pair ⟨ϱ,σ⟩ ,σ consisting of a Datalog rule ϱ=β→η =β→η and a substitution σ that is defined exactly on the set of all variables occurring in ϱ . The trigger τ is applicable to a fact set ℱF if σ(β)⊆ℱσ(β) and all constants in the range of σ occur in ℱF. We define (τ)=σ(η)Output(τ)=σ(η) and, for a fact set ℱF, we define ϱ(ℱ)App_ (F) as the set including (τ)Output(τ) for every trigger τ with ϱ that is applicable to ℱF. For a Datalog rule set ℛR and a fact set ℱF, let ℛ(ℱ)=⋃ϱ∈ℛϱ(ℱ)App_R(F)= _ App_ (F). For a Datalog KB =⟨ℛ,ℱ⟩K= ,F , let 1(),2(),…Ch_1(K),Ch_2(K),… be the sequence of fact sets such that (i) 1()=ℱCh_1(K)=F, and (i) i()=i−1()∪ℛ(i−1())Ch_i(K)=Ch_i-1(K) _R(Ch_i-1(K)) for every i≥2i≥ 2. We define the chase of K, written ()Ch(K), as the union of all fact sets in this sequence. By our definition of applicable triggers, the chase is always finite, and it yields a set of facts that can be used to decide fact entailment under active domain semantics [1]. Proposition 1 A Datalog KB K entails a fact α if and only if α∈()α (K). For a Datalog KB K, the chase depth of a fact α∈()α (K) with respect to K is the least k≥1k≥ 1 such that α∈k()α _k(K). 3 From Horn-ℒℋℐHorn-ALCHI to Horn-ℒ ／∃Horn-ALC_ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 1.36111pt -3.0128pt$ $ ∃ to0.0pt 0.97221pt -2.46837pt$ $ ∃ Queries This section briefly recalls how to normalize away axioms of the form (5), (6), and (7) from a Horn-ℒℋℐHorn-ALCHI rule set. Definition 1 A Horn-ℒ ／∃Horn-ALC_ to0.0pt 2.26389pt -4.24228pt$ $ ∃ to0.0pt 2.26389pt -4.24228pt$ $ ∃ to0.0pt 1.36111pt -3.07838pt$ $ ∃ to0.0pt 0.97221pt -2.53394pt$ $ ∃ rule is a rule of the form (1), (2), (3), or (4). Horn-ℒ ／∃Horn-ALC_ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 1.36111pt -3.0128pt$ $ ∃ to0.0pt 0.97221pt -2.46837pt$ $ ∃ queries and KBs are defined in the obvious way. To reduce to such rules, we proceed in two main steps. Assume we have a Horn-ℒℋℐHorn-ALCHI rule set ℛR. In the first step, we get rid of axioms of the forms (6) and (7). Let ⊑∗ ^* be the reflexive and transitive closure of the relation ⊑ induced by ℛR on RoleExps. Let ℛ′R be a copy of ℛR from which we remove all axioms of the forms (6) and (7) but add, for every ,∈ R, S∈ Roles such that ⊑∗ R ^* S or −⊑∗− R^- ^* S^-, the axioms: • (x)∧(x,y)→(y) A(x) R(x,y)→ B(y) for every axiom (x)∧(x,y)→(y) A(x) S(x,y)→ B(y) in ℛR; and • (x,y)∧(y)→(x) R(x,y) A(y)→ B(x) for every axiom (x,y)∧(y)→(x) S(x,y) A(y)→ B(x) in ℛR; and, for every ,∈ R, S∈ Roles such that −⊑∗ R^- ^* S or ⊑∗− R ^* S^-, the axioms: • (x,y)∧(y)→(x) R(x,y) A(y)→ B(x) for every axiom (x)∧(x,y)→(y) A(x) S(x,y)→ B(y) in ℛR; and • (x)∧(x,y)→(y) A(x) R(x,y)→ B(y) for every axiom (x,y)∧(y)→(x) S(x,y) A(y)→ B(x) in ℛR. It is then routine to verify that for every class fact α, the queries ⟨ℛ,α⟩ ,α and ⟨ℛ′,α⟩ ,α are equivalent. We here strongly rely on the queries being based upon class facts, as this procedure would fail already for those based on role facts. In the second step, we get rid of axioms of the form (5) by applying the translation to Datalog rules proposed in [10, Tables 2 and 3] for the more expressive Horn-ℋℐHorn-SHIQ. This reduction to their procedure is possible as our ℛ′R is already compliant with their notion of a Horn-ℋℐHorn-SHIQ rule set. We then remark that, given that we only input axioms of the forms (1)–(5) (or (F1), (F2), (F3) in the reference), their translation only outputs axioms of the form (1), (2), (3), or (4), as desired. In summary, we obtain the following: Theorem 3.1 There is a computable function mapping every Horn-ℒℋℐHorn-ALCHI query to an equivalent Horn-ℒ ／∃Horn-ALC_ to0.0pt 2.26389pt -4.24228pt$ $ ∃ to0.0pt 2.26389pt -4.24228pt$ $ ∃ to0.0pt 1.36111pt -3.07838pt$ $ ∃ to0.0pt 0.97221pt -2.53394pt$ $ ∃ query. Example 3 Consider the set of Horn-ℒ ／∃Horn-ALC_ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 1.36111pt -3.0128pt$ $ ∃ to0.0pt 0.97221pt -2.46837pt$ $ ∃ rules NFT_NF obtained from the set T from Example˜1 by removing (x)→∃y.(x,y)∧(y) Gate(x)→∃ y. Link(x,y) Onl(y) and adding (x)→(x) Gate(x)→ Onl(x). Furthermore, observe that the DL queries ⟨,(alice)⟩ , Trust(alice) and ⟨NF,(alice)⟩ _NF, Trust(alice) are equivalent. We observe that, in general, the resulting Horn-ℒ ／∃Horn-ALC_ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 1.36111pt -3.0128pt$ $ ∃ to0.0pt 0.97221pt -2.46837pt$ $ ∃ query has an exponential size compared to the original Horn-ℒℋℐHorn-ALCHI query. This blow-up arises in the second step and cannot be avoided and already occurs in the part of the translation borrowed from [10]: when removing even a single axiom of form (5), one may need exponentially-many axioms of form (1) to preserve equivalence of the rule queries. Such pathological cases can be extracted from proofs of the ExpTime-hardness of basic reasoning tasks already in Horn-ℒHorn-ALC, see e.g. [16]. 4 From Horn-ℒ ／∃Horn-ALC_ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 1.36111pt -3.0128pt$ $ ∃ to0.0pt 0.97221pt -2.46837pt$ $ ∃ Queries to DL Automata We introduce DL automata as finite-state devices closely related to regular tree automata, tailored to capture the expressive power of Horn-ℒ ／∃Horn-ALC_ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 1.36111pt -3.0128pt$ $ ∃ to0.0pt 0.97221pt -2.46837pt$ $ ∃ queries. We first formally introduce these in Definition˜2 and then explain their semantics in Definition˜3. Next, in Definition˜4, we present a reduction from Horn-ℒ ／∃Horn-ALC_ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 1.36111pt -3.0128pt$ $ ∃ to0.0pt 0.97221pt -2.46837pt$ $ ∃ queries to DL automata and show that this translation preserves the semantics of the input queries. Finally, in Remark˜1, we state some properties of the automata produced by this translation, which are applied in the following section to develop an equivalence-preserving reduction from a class of DL automata to PQs. Definition 2 We distinguish a special accepting state qaccq_acc. A binary transition is an expression of the form q↝Qq _ SQ, where q is a state, ∈ε∪ S∈\ \∪ Classes∪ RoleExps, and Q is a set of states with |Q|=1|Q|=1. A multi-ary transition is an expression of the form q↝εQq _ Q, where q is a state and Q is a set of states with |Q|≥2|Q|≥ 2. A transition is either a binary transition or a multi-ary transition. A DL automaton is a tuple ⟨s,Q,qinit,δ⟩ s,Q,q_init,δ , where s is a constant, Q is a finite set of states, qinitq_init is a state, and δ is a transition function over Q, that is, a finite set of transitions featuring only states in Q. Every DL automaton defines a boolean query and thereby partitions the set of all fact sets into those it accepts and those it rejects. As for rule queries and PQs, this partition is formalized by the “query mapping” function QM, defined below. To characterize the accepted fact sets, we first introduce the notion of a run of a DL automaton, analogous to a run of a tree automaton on a tree. Definition 3 A run of a DL automaton ⟨s,Q,qinit,δ⟩ s,Q,q_init,δ over a fact set ℱF from ⟨p,e⟩ p,e , where p is a state and e is a constant, is a triple ⟨N,E,L⟩ N,E,L such that: • The pair ⟨N,E⟩ N,E is a finite rooted directed tree. Moreover, L is a labeling function that maps every node to a pair consisting of a state and a constant, and maps the root to ⟨p,e⟩ p,e . • For every node n with L(n)=⟨q,c⟩L(n)= q,c that has exactly one child m in the tree, there is a binary transition q↝q′∈δq _ S\q \∈δ satisfying all of the following implications: (i) If =ε S= , then L(m)=⟨q′,c⟩L(m)= q ,c . (i) If S is a class, then (c)∈ℱ S(c) and L(m)=⟨q′,c⟩L(m)= q ,c . (i) If S is a role expression, then there is some constant d such that (c,d)∈ℱ∪(ℱ) S(c,d) (F) and L(m)=⟨q′,d⟩L(m)= q ,d . • For every node n with L(n)=⟨q,c⟩L(n)= q,c with at least two children m1,…,mkm_1,…,m_k, there is a multi-ary transition q↝εq1,…,qk∈δq _ \q_1,…,q_k\∈δ such that L(mi)=⟨qi,c⟩L(m_i)= q_i,c for every 1≤i≤k1≤ i≤ k. Such a run is accepting if all leaf labels in the tree feature the accepting state, and the constant s occurs in ℱF. A DL automaton =⟨s,qinit,Q,δ⟩ A= s,q_init,Q,δ accepts a fact set ℱF if there is an accepting run of A over ℱF from ⟨qinit,s⟩ q_init,s . Furthemore, let ()QM( A) be the set of all fact sets accepted by A. Such an automaton is contained in a rule query or a PQ γ if ()⊆(γ)QM( A) (γ); these two are equivalent if ()=(γ)QM( A)=QM(γ). q_ Trustqaccq_accq_ Gateq_ Sensq_ Critq_ Onl Link Link Trust− Acc^-ε Crit Sensε Onl Gaten1:⟨q,alice⟩n_1: q_ Trust,alice 2:⟨q,c1⟩n_2: q_ Crit,c_1 3r:⟨q,c1⟩n_3^r: q_ Sens,c_1 4r:⟨q,c2⟩n_4^r: q_ Sens,c_2 5r:⟨q,c3⟩n_5^r: q_ Sens,c_3 6r:⟨qacc,c3⟩n_6^r: q_acc,c_3 3ℓ:⟨q,c1⟩n_3 : q_ Onl,c_1 4ℓ:⟨q,c4⟩n_4 : q_ Onl,c_4 5ℓ:⟨q,c4⟩n_5 : q_ Gate,c_4 6ℓ:⟨qacc,c4⟩n_6 : q_acc,c_4 Figure 2: Consider the DL automaton ⟨alice,Q,q,δ⟩ ,Q,q_ Trust,δ , where δ is the transition function over Q depicted on the left, and the only accepting run of this automaton from ⟨q,alice⟩ q_ Trust,alice over the fact set ℱF introduced in Example˜1 depicted on the right. Example 4 In Figure˜2, we present a DL automaton together with one of its accepting runs over the fact set ℱF introduced in Example˜1. We will later argue that this automaton is equivalent to the Horn-ℒ ／∃Horn-ALC_ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 1.36111pt -3.0128pt$ $ ∃ to0.0pt 0.97221pt -2.46837pt$ $ ∃ query ⟨NF,(alice)⟩ _NF, Trust(alice) introduced in Example˜3; for now, the figure should help the reader understand why this automaton accepts this fact set. In the following definition, we present a reduction from Horn-ℒ ／∃Horn-ALC_ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 1.36111pt -3.0128pt$ $ ∃ to0.0pt 0.97221pt -2.46837pt$ $ ∃ queries to DL automata that preserves equivalence (cf. Example˜5). Definition 4 For every ∈ C∈ Classes, let q_ C be a fresh state unique for C. For a Horn-ℒ ／∃Horn-ALC_ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 1.36111pt -3.0128pt$ $ ∃ to0.0pt 0.97221pt -2.46837pt$ $ ∃ query γ=⟨ℛ,(s)⟩γ= , D(s) , let (γ)=⟨s,Q,q,δ⟩DLA(γ)= s,Q,q_ D,δ denote the DL automaton where Q is the set of states containing qaccq_acc and q_ C for every class C occurring in γ, and δ is the transition function containing all of the following: • For every class C occurring in γ, add q↝qacc∈δq_ C _ C\q_acc\∈δ. • For every rule such as ⋀i=1ni(x)→(x)∈ℛ ^n_i=1 A_i(x)→ B(x) , add q↝εq,…,q∈δq_ B _ \q_ A_1,…,q_ A_n\∈δ. • For every rule such as (x,y)∧(y)→(x)∈ℛ R(x,y) A(y)→ B(x) , add q↝q∈δq_ B _ R\q_ A\∈δ. • For every rule such as (x)∧(x,y)→(y)∈ℛ A(x) R(x,y)→ B(y) , add q↝−q∈δq_ B _ R^-\q_ A\∈δ. • For every rule such as →(x)∈ℛ→ B(x) , add q↝εqacc∈δq_ B _ \q_acc\∈δ. Example 5 Consider the rule set NFT_NF and the fact set ℱF introduced in Example˜1. Observe that the automaton (NF,(alice))DLA(T_NF, Trust(alice)), described in Figure˜2, accepts ℱF, as witnessed by the accepting run depicted in that same figure. By contrast, the automaton (NF,(bob))DLA(T_NF, Trust(bob)) does not accept ℱF, as there is no accepting run from ⟨q,bob⟩ q_ Trust,bob . restatable theoremCorrespondenceNormHornALCAutomata A Horn-ℒ ／∃Horn-ALC_ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 1.36111pt -3.0128pt$ $ ∃ to0.0pt 0.97221pt -2.46837pt$ $ ∃ query γ is equivalent to the DL automaton (γ)DLA(γ). Proof(Sketch) The theorem follows from the fact that, for every fact set ℱF and fact (b) B(b), the KB ⟨ℛ,ℱ⟩ ,F entails (b) B(b) if and only if there is an accepting run of (ℛ,(b))DLA(R, B(b)) over ℱF starting from ⟨q,b⟩ q_ B,b . The “if” direction is proved by induction on the height of the accepting run, while the “only if” direction is established by induction on the chase depth of (b) B(b) with respect to ⟨ℛ,ℱ⟩ ,F . To conclude the section, the following remark states several properties satisfied by every DL automaton produced by the reduction of Definition˜4. Remark 1 Consider a Horn-ℒ ／∃Horn-ALC_ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 1.36111pt -3.0128pt$ $ ∃ to0.0pt 0.97221pt -2.46837pt$ $ ∃ query γ and the DL automaton (γ)=⟨s,Q,qinit,δ⟩DLA(γ)= s,Q,q_init,δ . Then, all of the following hold: 1. There are no transitions originating from the accepting state; that is, δ does not contain transitions of the form qacc↝Pq_acc _ SP. 2. Every (binary) transition labelled with a class points to the accepting state; that is, for every q↝p∈δq _ C\p\∈δ with ∈ C∈ Classes, we have p=qaccp=q_acc. 3. Every non-final state directly reaches the accepting state through a binary transition; that is, for every q∈Q∖qaccq∈ Q \q_acc\, there is some transition of the form q↝qacc∈δq _ S\q_acc\∈δ. Properties 1 and 2 together ensure that transitions labelled with classes are considered only at the very end of an accepting run. This, in turn, simplifies the form of the regular expressions used in the following section to encode DL automata, since these only need to involve role expressions. Property 3 ensures that every state admits a path to the accepting state. If not for this restriction, a DL automaton may not accept any fact set. Such an automaton cannot be translated into a PQ, since the empty query is not a PQ under our definition. 5 From Stratified DL Automata to PQs In this section, we present an equivalence-preserving reduction from a class of DL automata to PQs. More precisely, this reduction applies only to stratified automata, which we formally introduce in the following definition. Definition 5 Consider a DL automaton =⟨s,Q,qinit,δ⟩ A= s,Q,q_init,δ . • For states q and p, we write q→2pq _ A^2p if δ contains a binary transition of the form q↝pq _ S\p\, and q→mpq _ A^mp if δ contains a multi-ary transition of the form q↝εPq _ P with p∈Pp∈ P. • We define → _ A as the union of →2 _ A^2 and →m _ A^m, and we define →∗ _ A^* as the reflexive transitive closure of → _ A. • For states q and p, we write q≻pq _ Ap if there are q′,q′,p′,p′∈Qq ,q ,p ,p ∈ Q and ∈ E∈ RoleExps with q→∗q′q _ A^*q , q′↝q′∈δq _ E\q \∈δ, q′→∗p′q _ A^*p , p′→mp′p _ A^mp , and p′→∗p _ A^*p. A DL automaton A is stratified if the relation ≻ _ A is acyclic, and if it satisfies the conditions in Remark˜1. If A is stratified, we define :Q→ℕStr_ A:Q as the function mapping a state q∈Qq∈ Q to 11 if q has no successors with respect to ≻ _ A, and to ((p)∣q≻p)+1Max(\Str_ A(p) q _ Ap\)+1 otherwise. Example 6 Consider the DL automaton =⟨alice,Q,q,δ⟩ A= ,Q,q_ Trust,δ described in Figure˜2. For instance, we have q≻q_ Trust _ Aq_ Gate, since all of the following hold: q→∗q↝−q∈δq→∗q q_ Trust _ A^*q_ Trust q_ Trust _ Acc^-\q_ Crit\∈δ q_ Crit _ A^*q_ Crit q→mqq→∗q q_ Crit _ A^mq_ Onl q_ Onl _ A^*q_ Gate Observe that A is stratified, since every cycle in its transition function involves only binary transitions. Our reduction from automata to PQs, formally introduced in Section˜5.2, proceeds by associating with every state q of a stratified DL automaton A a PQ describing the behaviour of A when started in q. This association is defined inductively: for states in stratum 11, the corresponding PQ is defined directly, whereas for states in stratum k≥2k≥ 2, it is defined using the PQs already associated with states in strictly lower strata. The role of stratification is to guarantee that this recursive construction is well defined. Indeed, the relation ≻ _ A captures precisely those dependencies between states that arise when the translation encounters a path containing a binary transition labelled with a role expression and, possibly after intermediate transitions, a multi-ary transition. In this situation, our inductive construction branches out and introduces additional existentially quantified variables, thereby producing formulas such as the third disjunct of the PQ in Example˜2. If cycles over ≻ _ A were allowed, the translation could follow the same dependencies indefinitely, repeatedly expanding the formula and introducing new existential variables, thus failing to produce a finite PQ. We point out that in Definition˜5 we require stratified automata to satisfy the conditions of Remark˜1, since these are necessary to prove some of the results that follow. This is without loss of generality when considering DL automata corresponding to Horn-ℒ ／∃Horn-ALC_ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 1.36111pt -3.0128pt$ $ ∃ to0.0pt 0.97221pt -2.46837pt$ $ ∃ queries since, as explained in the previous section, all such automata satisfy these conditions. We define our reduction from automata to PQs in Section˜5.2; its definition relies on a preliminary translation for DL automata without multi-ary transitions, presented in Section˜5.1. 5.1 DL Non-Deterministic Finite Automata In the following subsection, we present a reduction that transforms DL automata into equivalent PQs, that is, to positive FO formulas featuring regular expressions. To define such a transformation, we leverage existing automata-theoretic techniques defined for automata without multi-ary transitions. Definition 6 A DL non-deterministic finite automaton (NFA) A is a DL automaton without multi-ary transitions. Given states q and p, constants s and t, and a fact set ℱF, the automaton A transitions from ⟨q,s⟩ q,s to ⟨p,t⟩ p,t in ℱF if there is a run of A over ℱF from ⟨q,s⟩ q,s whose (unique) leaf is labelled with ⟨p,t⟩ p,t . Observe that, by Definition˜3, in every run of a DL automaton without multi-ary transitions, each node has at most one child; hence, such a run has exactly one leaf. It is well known from classical automata theory that the set of all paths induced by such an automaton can be characterized by a regular expression [14]. Lemma 1 Consider a DL NFA N that satisfies Remark˜1,333Recall that NFAs are DL automata by definition 6. and some states q and p of N such that p is different from qaccq_acc. Then, there is a regular expression q⊳p E_q p N such that, for every fact set ℱF and constants s and t, the NFA N can transition from ⟨q,s⟩ q,s to ⟨p,t⟩ p,t in ℱF if and only if ℱ⊧q⊳p(s,t)F E_q p N(s,t). Proof By Kleene’s theorem [15], there is a regular expression such as q⊳p E_q p N over role expressions such that (q⊳p)Lang( E_q p A) is the set of all words labelling the paths from q to p in N. This applies because no path from q to p visits the accepting state qaccq_acc since p≠qaccp≠ q_acc and qaccq_acc is a sink in N by Item 1 of Remark˜1. Therefore, these paths contain no classes, since by Item 2 of the same remark, all binary transitions of N labelled with classes have qaccq_acc as target. The previous auxiliary result allows us to readily define an equivalence-preserving reduction from NFAs to PQs. Definition 7 Given an NFA =⟨s,Q,qinit,δ⟩ N= s,Q,q_init,δ that satisfies Remark˜1, a state q of N, and a term t, we define NFA(,q,t)PQ_NFA( N,q,t) as the following PQ: • If q is the accepting state qaccq_acc, then this PQ is equal to ⊤ . • Otherwise, this PQ is the disjunction containing, for every p∈Q∖qaccp∈ Q \q_acc\ with q→∗pq _ N^*p, all of the following: (i) If p↝qacc∈p _ C\q_acc\∈ N for some ∈ C∈ Classes, add the disjunct ∃w.[q⊳p(t,w)∧(w)]∃ w. [ E_q p N(t,w) C(w) ] with w a fresh variable. (i) If p↝εqacc∈p _ \q_acc\∈ N, add the disjunct ∃w.q⊳p(t,w)∃ w. E_q p N(t,w) with w a fresh variable. Since N above satisfies Remark˜1, every state distinct from the accepting state reaches it via a binary transition annotated with a class. Therefore, the corresponding PQ is either ⊤ or a non-empty disjunction. restatable lemmalemmatransitioncrpq Consider a DL NFA N that satisfies Remark˜1, a fact set ℱF, a state q of N different from qaccq_acc, and a constant s in ℱF. There is an accepting run of N over ℱF starting at ⟨q,s⟩ q,s if and only if ℱF satisfies NFA(,q,s)PQ_NFA( N,q,s). The previous result yields an equivalence-preserving reduction from NFAs to PQs illustrated in the following example. Example 7 Consider the DL automaton ⟨alice,Q,q,δ⟩ ,Q,q_ Trust,δ depicted Figure˜2 and the NFA =⟨s,Q,q,δ′⟩ N= s,Q,q_ Onl,δ where δ′δ is the set of all binary transitions in δ. By Definition˜7, this NFA is equivalent to the following PQ: NFA(,q,s)=∃u1.[∗(s,u1)∧(u1)]∨∃u2.[∗(s,u2)∧(u2)]PQ_NFA( N,q_ Onl,s)=∃ u_1. [ Link^*(s,u_1) Onl(u_1) ] ∃ u_2. [ Link^*(s,u_2) Gate(u_2) ] In the following subsection, we use the previously discussed reduction as a subroutine in a more general translation applicable to stratified DL automata, which may contain multi-ary transitions. To apply this subroutine, we define the NFA reachable from a given state in a DL automaton. Definition 8 Given a DL automaton A and a state q of A, we define (,p)NFA( A,p) as the NFA obtained from A by performing the following modifications in sequence: remove all multi-ary transitions, remove all states that are not reachable from p through the remaining (binary) transitions, and remove all (binary) transitions that mention a state removed in the previous step. 5.2 An Inductive Reduction for Stratified DL Automata Before presenting our reduction, we define an extension of transition functions that allows adjacent ε -transitions to be handled in single step. Definition 9 For a transition function δ over a set of states Q, let δε∗δ^*_ be the (minimal) set of multi-ary transitions such that: For every q∈Qq∈ Q, we have q↝εq∈δε∗q _ \q\∈δ^*_ . For every q↝εP∈δε∗q _ P∈ _ ^* and p↝εP′∈δp _ P ∈δ with p∈Pp∈ P, we have q↝ε(P∖p)∪P′∈δε∗q _ (P \p\)∪ P ∈δ^*_ . Every DL automaton ⟨s,Q,qinit,δ⟩ s,Q,q_init,δ is equivalent to the extended automaton ⟨s,Q,qinit,δ∪δε∗⟩ s,Q,q_init,δ∪δ^*_ , since every transition in δε∗δ^*_ can be simulated by a finite sequence of ε -transitions already present in δ. Nevertheless, this extension allows every combination of states reachable via ε -transitions to be reached directly in a single step, thus avoiding potential cyclic dependencies in our reduction. In the following definition, we formally introduce our equivalence-preserving reduction, which is admittedly concise and technically involved. We suggest that the reader first skim through it, then consult the examples that follow, and only then return to the definition for a clearer understanding. Definition 10 Given a stratified DL automaton =⟨s,Q,qinit,δ⟩ A= s,Q,q_init,δ , a state q∈Qq∈ Q, a term t, we inductively define (,q,t)PQ( A,q,t) as the following PQ: ⋁q↝εP∈δε∗⋀p∈P(NFA(,p,t)∨ _q _ P∈δ^*_ _p∈ P (PQ_NFA( N,p,t)~ ⋁∀p′,p1,…,pn∈Q such that p→∗p′,p′↝εp1,…,pn,p≻p1,…, and p≻pn∃w.[p⊳p′(t,w)∧⋀i=1n(,pi,w)]) _ subarrayc∀ p ,p_1,…,p_n∈ Q such that p _ N^*p ,\\ p _ \p_1,…,p_n\,~p _ Ap_1,…, and p _ Ap_n subarray∃ w. [ E_p p N(t,w) _i=1^nPQ( A,p_i,w) ] ) In the above, N is the NFA (,q)NFA( A,q) and w is a fresh variable. In the following, we will sometimes write ()PQ( A) to refer to (,qinit,s)PQ( A,q_init,s). Observe that the above reduction is well defined since, for every stratified DL automaton A, the relation ≻ _ A is acyclic. Hence, we can first compute the PQs corresponding to all states in the lowest stratum, that is, states without successors with respect to ≻ _ A. We then proceed stratum by stratum, computing the subsequent PQs by relying on those obtained previously. The following example illustrates both the base case and the inductive step of our construction. Example 8 Consider the DL automaton A from Figure˜2 and a constant s. To illustrate the base case of our construction, we consider the state q_ Crit, which belongs to the lowest stratum of A, and present the corresponding PQ. (,q,s)= ( A,q_ Crit,s)=~ (NFA(,q,s)∧NFA(,q,s))∨ (PQ_NFA( N,q_ Sens,s) _NFA( N,q_ Onl,s) )\, (NFA(, (PQ_NFA( N, q,s)∧NFA(,q,s))∨NFA(,q,s) \,q_ Sens,s) _NFA( N,q_ Gate,s) )\, \,PQ_NFA( N,q_ Crit,s) NFA(,q,s)= _NFA( N,q_ Crit,s)=~ (s) Crit(s) NFA(,q,s)= _NFA( N,q_ Gate,s)=~ (s) Gate(s) NFA(,q,s)= _NFA( N,q_ Sens,s)=~ ∃u3.[∗(s,u3)∧(u3)] ∃ u_3. [ Link^*(s,u_3) Sens(u_3) ] The formula NFA(,q,s)PQ_NFA( N,q_ Onl,s) was already given in Example˜7. To illustrate the inductive step of our construction, we consider the state q_ Trust, which belongs to stratum 22 of A, and present the corresponding PQ. (,q,s)= ( A,q_ Trust,s)=~ (s)∨∃u4.[−(s,u4)∧(u4)]∨ Trust(s)\, \,∃ u_4. [ Acc^-(s,u_4) Crit(u_4) ]\, \, ∃u5.[−(s,u5) ∃ u_5. [ Acc^-(s,u_5) ∧(,q,u5)∧(,q,u5)] ( A,q_ Sens,u_5) ( A,q_ Onl,u_5) ] restatable theoremCorrespondenceAutomataCTRPQ A stratified DL automaton A is equivalent to ()PQ( A). Proof(Sketch) The theorem follows from the fact that, for every fact set ℱF and fact (b) B(b), the automaton A has an accepting run from ⟨q,b⟩ q_ B,b over ℱF if and only if ℱF entails (,q,b)PQ( A,q_ B,b). Both directions are proven by induction on the stratum of the state q_ B. 6 From Positive Queries to GQL Queries In this section, we show that PQs can be expressed in the Graph Query Language (GQL) [7, 11]. Namely, we present an equivalence-preserving mapping from PQs to a query language that is already known to be expressible in GQL [12]. Definition 11 A union of conjunctive two-way regular path queries (UC2RPQ) is a PQ of the form ⋁i=1n∃y→i.ψi _i=1^n∃ y_i. _i where all ψi _i are non-empty atom conjunctions. Definition 12 Given a PQ φ , we define (φ)UC2RPQ( ) as a PQ obtained by exhaustively applying the following replacement rules: 1. Replace a subformula of the form ∃w.(ψ∨ψ′)∃ w.(ψ ψ ) with (∃w.ψ)∨(∃v.ψ′[w/v])(∃ w.ψ) (∃ v.ψ [w/v]), where v is a fresh variable and ψ′[w/v]ψ [w/v] is the formula that results from replacing all occurrences of w in ψ′ψ with v. 2. Replace a subformula of the form (ψ1∧(ψ2∨ψ3))( _1 ( _2 _3)) with (ψ1∧ψ2)∨(ψ1∧ψ3)( _1 _2) ( _1 _3). 3. Replace a subformula of the form (∃w.ψ)∧(∃v.ψ′)(∃ w.ψ) (∃ v.ψ ) with ∃w,v.(ψ∧ψ′)∃ w,v.(ψ ψ ). The previous translation is included for completeness and is not an original contribution, as it relies on standard transformations [1, Chapter 5]. Lemma 2 For every PQ φ , the queries φ and (φ)UC2RPQ( ) are equivalent, and (φ)UC2RPQ( ) is a UC2RPQ. Proof One can prove the equivalence of the above formulas by induction on the sequence of formulas obtained by applying the replacement rules from Definition˜12 in the computation of (φ)UC2RPQ( ). Since the latter formula is obtained by exhaustively applying Rules 1 and 2, disjunctions occur only at the outermost level. Moreover, by the exhaustive application of Rule 3, conjunctions occur only at the innermost level. Therefore, (φ)UC2RPQ( ) is a UC2RPQ. The following is a corollary of the previous lemma and the equivalence-preserving reduction of unions of C2RPQs to GQL [12, Theorem 11]. Theorem 6.1 There is an equivalence-preserving reduction from PQs to GQL. 7 Related Work In the line of work on rewriting DL queries, a cornerstone is the first-order rewritability of rule queries of the DL-Lite family, allowing translation into unions of Select-Project-Join SQL queries [5]. It is worth noting that DL automata associated to (the positive versions) of DL-Lite rule queries are always stratified. Indeed, the popular fragments of DL-Lite (DL-Litecore, DL-LiteR) forbid axioms of the form (1) for n≥2n≥ 2. By unraveling the successive steps exposed in Section˜3, it is not difficult to verify that axioms of the form (1), for n≥2n≥ 2, are not introduced throughout the normalization procedure. Multi-ary transitions are therefore absent from the corresponding DL automata, which guarantees the existence of a stratification with a single stratum. Closer to our setting, rewriting of rule queries from (extensions of) ℰℒEL into queries based upon regular expressions has also been studied. In [8], rule queries of linear ℰℒEL are rewritten into regular-path queries, and this work was later extended to the so-called harmless linear ℰℒℋℐELHI [9] using UC2RPQs as a target query language. Harmless linear ℰℒℋℐELHI restricts axioms of the form (1) to the case of n=1n=1, as in DL-Lite, and limits the interaction of pairs of roles , S_1, S_2 whenever there exists a third role R such that both (x,y)→(x,y) R(x,y)→ S_1(x,y) and (x,y)→(y,x) R(x,y)→ S_2(y,x) are entailed by the set of rules. Already due to the restriction on conjunction, Example˜2 falls outside of the rule queries that their approach can rewrite. The nature of the restrictions in harmless linear ℰℒℋℐELHI makes a more formal comparison with our approach difficult. We have not found an example of a harmless linear ℰℒℋℐELHI rule query that does not have an associated stratified DL automaton. More recently, and also motivated by the navigational features of GQL, quasi-linear ℰℒℋELH with limited inverses (ℰℒℋiqlELH^ql_i) was introduced and has been shown to enjoy rewriting into UC2RPQs [18]. The definition of this latter extension of ℰℒEL is characterized by a notion of locality. Typically, our axiom (x)∧(x,y)→(y) Crit(x) Acc(x,y)→ Trust(y) makes the class Crit non-local, and ℰℒℋiqlELH^ql_i forbids non-local classes from appearing in the head of an axiom of form 1. As a consequence, an axiom like (x)∧(x)→(x) Sens(x) Onl(x)→ Crit(x) is not allowed in ℰℒℋiqlELH^ql_i. This shows that Example 2 is not a ℰℒℋiqlELH^ql_irule query, while being rewritable with our approach since its corresponding DL automaton is stratified (see Example 6). We speculate that by examining closely how the notion of (non-)locality is preserved through the different normalization steps exposed in Section˜3, one can establish that every ℰℒℋiqlELH^ql_i rule query has an associate stratified DL automaton. Together with the previous remark regarding Example 2, such a verification would guarantee that our work strictly subsumes theirs. A very recent work [2] has also pinpointed a subclass of ℰℒℋℐELHI queries that supports rewriting into nested 2RPQs, another fragment of GQL. The proposed subclass, namely ℰℒℐ⪯⊥ELI _ , relies on the existence of a stratification of class and role expressions, constrained by the rule set. This stratification notably limits recursion to rules with shape (x,y)∧(y)→(x) R(x,y) A(y)→ A(x) or (x)∧(x,y)→(y) A(x) R(x,y)→ A(y). As a consequence, their approach cannot rewrite the query ⟨(x,y)∧(y)→(x),(x,y)∧(y)→(x),(a)⟩ \ R(x,y) A(y)→ B(x), R(x,y) B(y)→ A(x)\, A(a) , whose corresponding DL automaton is trivially stratified. Their work also seemingly varies from ours as the nested 2RPQs they consider support tests along the 2RPQs. However, we did not find an example of an ℰℒℐ⪯⊥ELI _ query that is not already rewritable using our approach; a natural candidate exploiting the presence of tests in their formalism would have been the rule query ⟨(x)∧(x)→(x),(x,y)∧(y)→(x),(c)⟩ \ A(x) B(x)→ C(x), R(x,y) C(y)→ A(x)\, C(c) , but both approaches fail to rewrite this query. 8 Conclusions and Future Work As our main contribution, we define an equivalence-preserving procedure that transforms a class of Horn-ℒℋℐHorn-ALCHI queries into equivalent GQL formulas, proceeding in several steps. First, an input Horn-ℒℋℐHorn-ALCHI query is transformed into a Horn-ℒ ／∃Horn-ALC_ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 1.36111pt -3.0128pt$ $ ∃ to0.0pt 0.97221pt -2.46837pt$ $ ∃ query (Theorem˜3.1), which is then translated into a DL automaton (Example˜5). If the resulting automaton is stratified, it can be further translated into a PQ (Example˜8), and subsequently into a GQL query (Theorem˜6.1). An immediate direction for future work is to extend our translation to handle other constructors available in standard DL languages. For instance, our technique can be readily adapted to incorporate disjointness rules of the form (x)∧…∧(x)→⊥ A_1(x) … A_n(x)→ , which are typically allowed in Horn DLs [16]. When computing the rewriting of a Horn-ℒℋℐHorn-ALCHI query ⟨ℛ,(a)⟩ , A(a) in the presence of such rules, we may treat ⊥ as a normal class and instead compute a GQL rewriting for the rule query ⟨ℛ,(a)∨∃w.⊥(w)⟩ , A(a) ∃ w. (w) ; similar ideas have already been considered in e.g. [4]. This approach is correct since, for every fact set ℱF, the following hold: the KB ⟨ℛ,ℱ⟩ ,F is unsatisfiable if and only if it entails ∃w.⊥(w)∃ w. (w); and ⟨ℛ,ℱ⟩ ,F entails (a) A(a) if and only if it is unsatisfiable, or ⟨ℛ ／⊥,ℱ⟩⊧(a) _ to0.0pt 3.125pt -4.17671pt$ $ to0.0pt 3.125pt -4.17671pt$ $ to0.0pt 1.90555pt -3.0128pt$ $ to0.0pt 1.36111pt -2.46837pt$ $ ,F A(a) with ℛ ／⊥R_ to0.0pt 3.125pt -4.17671pt$ $ to0.0pt 3.125pt -4.17671pt$ $ to0.0pt 1.90555pt -3.0128pt$ $ to0.0pt 1.36111pt -2.46837pt$ $ the subset of ℛR without syntactic occurrences of ⊥ . Extending our translation to other DL constructors, such as role chains, is likely to be more challenging. Nevertheless, complex roles appear amenable to our approach, since these closely correspond to regular languages [6, 21] and could in principle be handled using the techniques from Section˜5.1. Another direction for future work is to relax the stratification condition in Definition˜5 to capture a broader class of Horn-ℒℋℐHorn-ALCHI queries expressible in GQL. Indeed, our approach is not complete and fails to characterise queries such as ⟨(x)∧(x)→(x),(x,y)∧(x)→(x),(x,y)∧(x)→(x),(c)⟩ \ A(x) B(x)→ C(x), R(x,y) A(x)→ A(x), S(x,y) C(x)→ B(x)\, C(c) because this query is not equivalent to a PQ. Nevertheless, it can be translated into an equivalent nested regular path query, which can in turn be expressed in GQL [12, Theorem 11]. Considering nested regular path queries as a target language for our rewritings may therefore lead to a more general procedure. Before diving into a deeper theoretical study, an empirical evaluation of our approach may be useful. Namely, one could consider a collection of real-world Horn-ℒℋℐHorn-ALCHI rule sets [20] and determine which are captured by our method, that is, determine how many correspond to a stratified DL automaton (cf. Definitions˜4 and 5). This would help assess (i) whether our translation procedure is sufficiently general to be useful in practice, and (i) whether simple modifications could be introduced to capture existing queries outside its current scope. Finally, another relevant direction for future work is to characterize those Horn-ℒℋℐHorn-ALCHI queries that do not admit an equivalent GQL formulation. In particular, one could aim to obtain results analogous to those in [19], which provide a decidable and complete characterization of ℰℒEL queries that admit rewritings into first-order logic and linear Datalog. Our translation into DL automata presented in Section˜4 may prove useful in this regard, as it could enable the transfer of techniques from automata theory, a well-developed area of theoretical computer science, for establishing inexpressibility results. Acknowledgements. This research was funded by the Agence Nationale de la Recherche (ANR) under the Expand project (ANR-25-CE23-1215) and the France 2030 project (ANR-23-IACL-0008). References [1] S. Abiteboul, R. Hull, and V. Vianu (1995) Foundations of databases. Addison-Wesley. External Links: ISBN 0-201-53771-0 Cited by: §2, §6. [2] J. Arpasi, B. J. Bednarczyk, and M. Ortiz (2026) A Horn extension of DL-Lite with NL data complexity. In Proceedings of the 39th International Workshop on Description Logics (DL 2026), CEUR Workshop Proceedings, Vol. 4230. External Links: Link Cited by: §7. [3] F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi, and P. F. Patel-Schneider (Eds.) (2003) The description logic handbook: theory, implementation, and applications. Cambridge University Press. External Links: ISBN 0-521-78176-0 Cited by: §1. [4] A. Calì, G. Gottlob, and T. Lukasiewicz (2012) A general datalog-based framework for tractable query answering over ontologies. J. Web Semant. 14, p. 57–83. External Links: Link Cited by: §8. [5] D. Calvanese, G. De Giacomo, D. Lembo, M. Lenzerini, and R. Rosati (2007) Tractable reasoning and efficient query answering in description logics: the DL-Lite family. Journal of Automated Reasoning (JAR) 39 (3), p. 385–429. External Links: ISSN 1573-0670, Link Cited by: Appendix 0.D, §7. [6] D. Carral, L. González, and P. Koopmann (2019) From Horn-ℛℐSRIQ to datalog: A data-independent transformation that preserves assertion entailment. In Proceedings of the 33rd AAAI Conference on Artificial Intelligence (AAAI 2019), p. 2736–2743. External Links: Link Cited by: §8. [7] A. Deutsch, N. Francis, A. Green, K. Hare, B. Li, L. Libkin, T. Lindaaker, V. Marsault, W. Martens, J. Michels, F. Murlak, S. Plantikow, P. Selmer, O. van Rest, H. Voigt, D. Vrgoč, M. Wu, and F. Zemke (2022) Graph pattern matching in GQL and SQL/PGQ. In Proceedings of the 2022 International Conference on Management of Data (SIGMOD 2022), p. 2246–2258. External Links: Document Cited by: §1, §6. [8] M. M. Dimartino, A. Calì, A. Poulovassilis, and P. T. Wood (2016) Query rewriting under linear el knowledge bases. In Web Reasoning and Rule Systems, p. 61–76. External Links: ISBN 978-3-319-45276-0 Cited by: §7. [9] M. M. Dimartino, P. T. Wood, A. Calì, and A. Poulovassilis (2025) Efficient ontology-mediated query answering: extending DL-liteR and linear ℰℒℋELH. Journal of Artificial Intelligence Research 82, p. 851–899. External Links: Link Cited by: §7. [10] T. Eiter, M. Ortiz, M. Simkus, T. Tran, and G. Xiao (2021) Query rewriting for Horn-ℋℐSHIQ plus rules. Proceedings of the 35th AAAI Conference on Artificial Intelligence (AAAI 2021) 26 (1), p. 726–733. External Links: Link Cited by: Appendix 0.A, Appendix 0.D, §3, §3. [11] N. Francis, A. Gheerbrant, P. Guagliardo, L. Libkin, V. Marsault, W. Martens, F. Murlak, L. Peterfreund, A. Rogova, and D. Vrgoč (2023) A Researcher’s Digest of GQL. In Proceedings of the 26th International Conference on Database Theory (ICDT 2023), Vol. 255, p. 1:1–1:22. External Links: Document Cited by: §1, §6. [12] N. Francis, A. Gheerbrant, P. Guagliardo, L. Libkin, V. Marsault, W. Martens, F. Murlak, L. Peterfreund, A. Rogova, and D. Vrgoc (2023) GPC: a pattern calculus for property graphs. In Proceedings of the 42nd ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems (PODS 2023), p. 241–250. External Links: Document Cited by: §6, §6, §8. [13] P. Hitzler, M. Krötzsch, and S. Rudolph (2010) Foundations of semantic web technologies. Chapman and Hall/CRC Press. External Links: Link, ISBN 9781420090505 Cited by: §1. [14] J. E. Hopcroft, R. Motwani, and J. D. Ullman (2007) Introduction to automata theory, languages, and computation, 3rd edition. Pearson international edition, Addison-Wesley. External Links: ISBN 978-0-321-47617-3 Cited by: §5.1. [15] J. E. Hopcroft and J. D. Ullman (1979) Introduction to automata theory, languages and computation. Addison-Wesley. Cited by: §5.1. [16] M. Krötzsch, S. Rudolph, and P. Hitzler (2013) Complexities of horn description logics. ACM Transactions on Computational Logic (TOCL) 14 (1), p. 2:1–2:36. External Links: Link Cited by: §2, §3, §8. [17] M. Krötzsch, F. Simancik, and I. Horrocks (2012) A description logic primer. CoRR abs/1201.4089. External Links: Link, 1201.4089 Cited by: footnote 1. [18] B. Löhnert, N. Augsten, C. Okulmus, and M. Ortiz (2025) Towards practicable algorithms for rewriting graph queries beyond DL-Lite. In The Semantic Web, E. Curry, M. Acosta, M. Poveda-Villalón, M. van Erp, A. Ojo, K. Hose, C. Shimizu, and P. Lisena (Eds.), p. 342–361. External Links: ISBN 978-3-031-94575-5 Cited by: §1, §7. [19] C. Lutz and L. Sabellek (2022) A complete classification of the complexity and rewritability of ontology-mediated queries based on the description logic EL. Artificial Intelligence 308, p. 103709. External Links: Link Cited by: §8. [20] N. Matentzoglu, D. Tang, B. Parsia, and U. Sattler (2014) The manchester OWL repository: system description. In Proceedings of the 13th International Semantic Web Conference, (ISWC 2014), Posters & Demonstrations Track, CEUR Workshop Proceedings, p. 285–288. External Links: Link Cited by: §8. [21] F. Simancík (2012) Elimination of complex RIAs without automata. In Proceedings of the 25th International Workshop on Description Logics (DL 2012), Y. Kazakov, D. Lembo, and F. Wolter (Eds.), CEUR Workshop Proceedings. External Links: Link Cited by: §8. Appendix 0.A Proofs of Section˜3 In this section, we prove the claims leading to Theorem˜3.1. Let ⟨ℛ,α⟩ ,α be a Horn-ℒℋℐHorn-ALCHI query, and ℛ′R the rule set obtained as described in Section˜3. We first verify that ⟨ℛ,α⟩ ,α and ⟨ℛ′,α⟩ ,α are equivalent. Notice that axioms from ℛ′R are consequences of ℛR, and thus it is clear that (ℛ′,α)⊆(ℛ,α)QM(R ,α) (R,α). It remains to prove the converse, that is the following lemma. Lemma 3 (ℛ′,α)⊇(ℛ,α)QM(R ,α) (R,α). Proof Let ℱF be a fact set such that ⟨ℛ,ℱ⟩⊧α ,F α, we need to prove that ⟨ℛ′,ℱ⟩⊧α ,F α. Let ℐI be an FO-model of ⟨ℛ′,ℱ⟩ ,F , we denote Δℐ ^I its domain and ⋅ℐ·^I its interpretation function. We construct an FO-structure J that extends ℐI and will be a model of ⟨ℛ,ℱ⟩ ,F . The domain of J is also Δℐ ^I, it interprets every class as in ℐI, and every role ∈ R∈ Roles as follows: :=⋃∈s.t. ⊑∗ℐ. R^J:= _ subarrayc S∈ RoleExps\\ s.t.\ S ^* R subarray S^I. We further refer to the property that, by definition, J and ℐI agree on the interpretation of classes as (⋆)( ). We now verify that J is a model of ⟨ℛ,ℱ⟩ ,F , which will conclude the proof since it guarantees ⊧αJ α using the assumption that ⟨ℛ,ℱ⟩⊧α ,F α and consequently ℐ⊧αI α by (⋆)( ). It is clear that ⊧ℱJ , it thus remains to verify ⊧ℛJ . We examine each possible form of axiom in ℛR: (1) Immediate by (⋆)( ). (2) Assume (x,y)∧(y)→(x)∈ℛ R(x,y) A(y)→ B(x) , (d,e)∈(d,e)∈ R^J and e∈e∈ A^J. By definition of ℛ′R , we have (x,y)∧(y)→(x)∈ℛ′ R(x,y) A(y)→ B(x) and, by (⋆)( ), we have e∈ℐe∈ A^I. By definition of R^J, we have (d,e)∈ℐ(d,e)∈ S^I for some ⊑∗ S ^* R. Now, either ∈ S∈ Roles, and then we have (x,y)∧(y)→(x)∈ℛ′ S(x,y) A(y)→ B(x) by definition of ℛ′R , or ∈ S∈ InvRoles and we have (x)∧(x,y)→(y)∈ℛ′ A(x) S(x,y)→ B(y) . Either way, ℐ⊧ℛ′I yields d∈ℐd∈ B^I, and we conclude using (⋆)( ). (3) Assume (x)∧(x,y)→(y)∈ℛ A(x) R(x,y)→ B(y) , (d,e)∈(d,e)∈ R^J and d∈d∈ A^J. By definition of ℛ′R , we have (x)∧(x,y)→(y)∈ℛ′ A(x) R(x,y)→ B(y) and, by (⋆)( ), we have d∈ℐd∈ A^I. By definition of R^J, we have (d,e)∈ℐ(d,e)∈ S^I for some ⊑∗ S ^* R. Now, either ∈ S∈ Roles, and then we have (x)∧(x,y)→(y)∈ℛ′ A(x) S(x,y)→ B(y) by definition of ℛ′R , or ∈ S∈ InvRoles and we have (x,y)∧(y)→(x)∈ℛ′ S(x,y) A(y)→ B(x) . Either way, ℐ⊧ℛ′I yields e∈ℐe∈ B^I, and we conclude using (⋆)( ). (4) Immediate by (⋆)( ). (5) Assume (x)→∃y.(x,y)∧(y)∈ℛ A(x)→∃ y. R(x,y) B(y) and d∈d∈ A^J. By definition of ℛ′R , we have (x)→∃y.(x,y)∧(y)∈ℛ′ A(x)→∃ y. R(x,y) B(y) and, by (⋆)( ), we have d∈ℐd∈ A^I. Since ℐ⊧ℛ′I , there exists e∈ℐe∈ B^I such that (d,e)∈ℐ(d,e)∈ R^I. Using that ⊑∗ ^* is reflexive, the definition of R^J yields (d,e)∈(d,e)∈ R^J. Using (⋆)( ), we obtain e∈e∈ B^J and we are done. (6) Immediate by construction of J and ⊑∗ ^* being transitive. (7) Immediate by construction of J and ⊑∗ ^* being transitive. We now explain how the Datalog translation proposed in [10] can be applied to ℛ′R . Let us highlight that ℛ′R complies with the normal form demanded in [10]: axioms of ℛ′R with forms (1) or (4) are exactly in their form (F1); those with forms (2) or (3) are exactly in their form (F2) (since the latter supports inverse roles!); and those with form (5) are exactly in their form (F3). In particular, ℛ′R does not contain any axiom in their form (F4). In turn, it follows that, when applying the inference rules from Table 2 in [10], their Rules ≤R_≤ and ≤−R^-_≤ are never applied. The same holds for their Rule ⊑rR^r_ since ℛ′R does not contain role inclusions, and Rule ⊥R_ since we restricted our attention to positive Horn-ℒℋℐHorn-ALCHI rules. These observations further guarantee that, applying the final translation in Table 3 [10], only the first two completion rules are ever applied. Therefore, we obtain a set ℛ′R of Datalog rules whose rules are of form B(y)←A(x),r(x,y)B(y)← A(x),r(x,y) and B(x)←A1(x),…,An(x)B(x)← A_1(x),…,A_n(x), where r is possibly an inverse role. Now, B(x)←A1(x),…,An(x)B(x)← A_1(x),…,A_n(x) rules are either in forms (1) or (4) in our formalism, while B(y)←A(x),r(x,y)B(y)← A(x),r(x,y) rules are either in form (3) if r∈r∈ Roles, or in form (2) if r∈r∈ InvRoles. Altogether, we obtained a set ℛ′R of Horn-ℒ ／∃Horn-ALC_ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 1.36111pt -3.0128pt$ $ ∃ to0.0pt 0.97221pt -2.46837pt$ $ ∃ rules such that, for every class fact α, ⟨ℛ′,α⟩ ,α is equivalent to ⟨ℛ′,α⟩ ,α [10, Theorem 3], thus equivalent to ⟨ℛ,α⟩ ,α . This concludes the proof of Theorem 3.1. Appendix 0.B Proofs of Section˜4 In this section, we prove Example˜5, which establishes the equivalence between a Horn-ℒ ／∃Horn-ALC_ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 1.36111pt -3.0128pt$ $ ∃ to0.0pt 0.97221pt -2.46837pt$ $ ∃ query γ and the corresponding automaton (γ)DLA(γ). More precisely, we prove Lemmas˜5 and 4, from which the theorem follows directly as a corollary. Lemma 4 A Horn-ℒ ／∃Horn-ALC_ to0.0pt 2.26389pt -4.24228pt$ $ ∃ to0.0pt 2.26389pt -4.24228pt$ $ ∃ to0.0pt 1.36111pt -3.07838pt$ $ ∃ to0.0pt 0.97221pt -2.53394pt$ $ ∃ query γ is contained in the DL automaton (γ)DLA(γ). Proof We fix a Horn-ℒ ／∃Horn-ALC_ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 1.36111pt -3.0128pt$ $ ∃ to0.0pt 0.97221pt -2.46837pt$ $ ∃ query γ=⟨ℛ,(a)⟩γ= , A(a) , the DL automaton (γ)=⟨a,Q,q,δ⟩DLA(γ)= a,Q,q_ A,δ , and a fact set ℱF. To prove the lemma, we assume that ℱ∈(γ)F (γ) and show that this implies ℱ∈((γ))F (DLA(γ)). More precisely, we establish that for any given fact (b)∈(ℛ,ℱ) B(b) (R,F), there is an accepting run of (ℛ,(b))DLA(R, B(b)) over ℱF from ⟨q,b⟩ q_ B,b . Applying this claim to the fact (a) A(a), we obtain an accepting run of (γ)DLA(γ) over ℱF from ⟨q,a⟩ q_ A,a , and therefore ℱ∈((γ))F (DLA(γ)). We prove the claim by induction on the depth of (b) B(b) with respect to ⟨ℛ,ℱ⟩ ,F . Recall also that (b)∈(ℛ,ℱ) B(b) (R,F) if and only if ⟨ℛ,ℱ⟩⊧(b) ,F B(b) by Proposition˜1. For the base case, we assume that (b) B(b) has depth 1 with respect to ⟨ℛ,ℱ⟩ ,F , which implies that (b)∈ℱ B(b) . Consider now the directed labelled tree ⟨r,r′,r→r′,L⟩ \r,r \,\r→ r \,L , where L is the labelling function mapping r to ⟨q,b⟩ q_ B,b and r′r to ⟨qacc,b⟩ q_acc,b . This tree is an accepting run of (γ)DLA(γ) over ℱF from ⟨q,b⟩ q_ B,b . Observe that it has a unique leaf labelled with the accepting state. Moreover, the edge r→r′r→ r is valid, since (b)∈ℱ B(b) and q↝qacc∈δq_ B _ B\q_acc\∈δ. For the induction step, we assume that (b) B(b) has depth k≥2k≥ 2 with respect to ⟨ℛ,ℱ⟩ ,F . Then at least one of the following cases applies: • There is a rule of the form (x,y)∧(y)→(x)∈ℛ R(x,y) C(y)→ B(x) and a constant c such that (b,c),(c)∈k−1(ℛ,ℱ) R(b,c), C(c) _k-1(R,F). By induction hypothesis, there is an accepting run ⟨N,E,L⟩ N,E,L of (ℛ,(c))DLA(R, C(c)) over ℱF from ⟨q,c⟩ q_ C,c . Consider the directed labelled tree ⟨N′,E′,L′⟩ N ,E ,L where N′=N∪rN =N∪\r\ for some fresh node r, E′=E∪r→r′E =E∪\r→ r \ where r′r is the root node of ⟨N,E,L⟩ N,E,L , and L′L is the function that extends L and maps r to ⟨q,b⟩ q_ B,b . We argue that ⟨N′,E′,L′⟩ N ,E ,L is an accepting run for (ℛ,(b))DLA(R, B(b)) over ℱF from ⟨q,b⟩ q_ B,b : – Since (x,y)∧(y)→(x)∈ℛ R(x,y) C(y)→ B(x) , we have that q↝q∈δq_ B _ R\q_ C\∈δ. Since no rule allows the derivation of binary facts, we have that (b,c)∈ℱ R(b,c) , which implies that the edge r→r′r→ r is valid as per Definition˜3. Therefore ⟨N′,E′,L′⟩ N ,E ,L is a run, as all other edges in this tree satisfy the same definition by induction hypothesis. – The leaves in ⟨N′,E′,L′⟩ N ,E ,L are exactly the leaves of ⟨N,E,L⟩ N,E,L . Hence, all of the leaves in ⟨N′,E′,L′⟩ N ,E ,L feature the accepting state. • There is a rule of the form (y)∧(x,y)→(x)∈ℛ C(y) R(x,y)→ B(x) and a constant c such that (c),(c,b)∈k−1(ℛ,ℱ) C(c), R(c,b) _k-1(R,F). This case is analogous to the previous one. • There is a rule of the form 1(x)∧…∧n(x)→(x)∈ℛ C_1(x) … C_n(x)→ B(x) with 1(b),…,n(b)∈k−1(ℛ,ℱ) C_1(b),…, C_n(b) _k-1(R,F). By induction hypothesis, there is an accepting run ⟨Ni,Ei,Li⟩ N_i,E_i,L_i of (ℛ,i(b))DLA(R, C_i(b)) over ℱF from ⟨qi,b⟩ q_ C_i,b for every 1≤i≤n1≤ i≤ n. Consider the directed labeled tree ⟨N′,E′,L′⟩ N ,E ,L where N′=N1∪…∪Nn∪rN =N_1∪…∪ N_n∪\r\ with r a fresh node, E′=E1∪…∪En∪r→r1,…,r→rnE =E_1∪…∪ E_n∪\r→ r_1,…,r→ r_n\ with rir_i the root node of ⟨Ni,Ei,Li⟩ N_i,E_i,L_i for every 1≤i≤n1≤ i≤ n, and L′L is the function that extends Li∪…∪LnL_i∪…∪ L_n and maps r to ⟨q,b⟩ q_ B,b . We argue that ⟨N′,E′,L′⟩ N ,E ,L is an accepting run for (ℛ,(b))DLA(R, B(b)) over ℱF from ⟨q,b⟩ q_ B,b : – As 1(x)∧…∧n(x)→(x)∈ℛ C_1(x) … C_n(x)→ B(x) , we have that q↝εq1,…,qn∈δq_ B _ \q_ C_1,…,q_ C_n\∈δ. This implies that the edges r→r1r→ r_1 through r→rnr→ r_n in E′E are valid as per Definition˜3. Therefore ⟨N′,E′,L′⟩ N ,E ,L is a run, as all other edges in this tree satisfy the same definition by induction hypothesis. – The leaves in ⟨N′,E′,L′⟩ N ,E ,L are exactly the union of the leaves of the ⟨Ni,Ei,Li⟩ N_i,E_i,L_i . Hence, all of the leaves in ⟨N′,E′,L′⟩ N ,E ,L feature the accepting state. • There is a rule of the form →(x)∈ℛ→ B(x) . Consider the directed labelled tree ⟨r,ℓ,r→ℓ,L⟩ r, ,r→ ,L , where L maps r to ⟨q,b⟩ q_ B,b and ℓ to ⟨qacc,b⟩ q_acc,b . This tree is an accepting run of (ℛ,(b))DLA(R, B(b)) over ℱF starting from ⟨q,b⟩ q_ B,b . Note that q↝εqacc∈δq_ B _ \q_acc\∈δ since →(x)∈ℛ→ B(x) . In either case, there is an accepting run of (ℛ,(b))DLA(R, B(b)) over ℱF from ⟨q,b⟩ q_ B,b . Lemma 5 A Horn-ℒ ／∃Horn-ALC_ to0.0pt 2.26389pt -4.24228pt$ $ ∃ to0.0pt 2.26389pt -4.24228pt$ $ ∃ to0.0pt 1.36111pt -3.07838pt$ $ ∃ to0.0pt 0.97221pt -2.53394pt$ $ ∃ query γ contains the DL automaton (γ)DLA(γ). Proof We fix a Horn-ℒ ／∃Horn-ALC_ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 2.26389pt -4.17671pt$ $ ∃ to0.0pt 1.36111pt -3.0128pt$ $ ∃ to0.0pt 0.97221pt -2.46837pt$ $ ∃ query γ=⟨ℛ,(a)⟩γ= , A(a) and a fact set ℱF. To prove the lemma, we assume that ℱ∈((γ))F (DLA(γ)) and show that ℱ∈(γ)F (γ). More precisely, we argue that, given some fact (b) B(b), if there is an accepting run of (ℛ,(a))DLA(R, A(a)) over ℱF from ⟨q,b⟩ q_ B,b , then (b)∈(ℛ,ℱ) B(b) (R,F). This implies in particular that (a)∈(ℛ,ℱ) A(a) (R,F), and therefore that ℱ∈(γ)F (γ). The proof proceeds by induction on the height of the accepting run of the fact (b) B(b). Recall that a fact is entailed by ⟨ℛ,ℱ⟩ ,F if and only if it is in (ℛ,ℱ)Ch(R,F) by Proposition˜1. Given some fact (b) B(b), there is no accepting run of (ℛ,(a))DLA(R, A(a)) over ℱF from ⟨q,b⟩ q_ B,b of height 11. Indeed, the unique node of such a run would have to feature both q_ B and qaccq_acc in its label, which is impossible since these are distinct states. Hence, the base case of our induction starts with runs of height 22. Regarding the base case, we assume that there is an accepting run of (ℛ,(a))DLA(R, A(a)) over ℱF from ⟨q,b⟩ q_ B,b of height 2. In this case, the root node of this run is labelled ⟨q,b⟩ q_ B,b and all of the labels of its children feature the accepting state. Therefore, there are only two possible cases: • We have that (b)∈ℱ B(b) . Note that q↝qaccq_ B _ B\q_acc\ is a transition of (γ)DLA(γ). • We have that q↝εqaccq_ B _ \q_acc\ is a transition of (γ)DLA(γ). Note that, in this case, we have that →(x)∈ℛ→ B(x) . In either case, we have that (b)∈(ℛ,ℱ) B(b) (R,F). Recall that b occurs in ℱF since there is an accepting run of (ℛ,(a))DLA(R, A(a)) over ℱF from ⟨q,b⟩ q_ B,b . Regarding the induction step, let us consider an accepting run ⟨N,E,L⟩ N,E,L for (γ)DLA(γ) over ℱF from ⟨q,b⟩ q_ B,b of height k>2k>2. We consider two different cases depending if the root node r of this run has one child or more. • Assume that the root r has a unique child r′r , which does not feature qaccq_acc in its label by Remark˜1. Then, by Definition˜3 and Remark˜1, one of the following cases must hold: – There is some class C such that r′r is labelled with ⟨q,b⟩ q_ C,b , q↝εq∈(γ)q_ B _ \q_ C\ (γ), and (b)∈ℱ C(b) . Now consider the tree ⟨N′,E′,L′⟩ N ,E ,L obtained by removing r from ⟨N,E,L⟩ N,E,L , which is of height k−1k-1 and is an accepting run for (γ)DLA(γ) from ⟨q,b⟩ q_ C,b over ℱF. Hence, (b)∈(ℛ,ℱ) C(b) (R,F) by induction hypothesis. Therefore, (b)∈(ℛ,ℱ) B(b) (R,F) since (x)→(x)∈ℛ C(x)→ B(x) . – There are a class C and a constant c such that r′r is labelled with ⟨q,c⟩ q_ C,c , q↝q∈(γ)q_ B _ Rq_ C (γ), and (b,c)∈ℱ R(b,c) . Now consider the tree ⟨N′,E′,L′⟩ N ,E ,L obtained by removing r from ⟨N,E,L⟩ N,E,L , which is of height k−1k-1 and is accepting for (ℛ,(c))DLA(R, C(c)) over ℱF from ⟨q,c⟩ q_ C,c . Hence, (c)∈(ℛ,ℱ) C(c) (R,F) by the induction hypothesis. Therefore, (b)∈(ℛ,ℱ) B(b) (R,F) since (x,y)∧(y)→(x)∈ℛ R(x,y) C(y)→ B(x) . – There are a class C and a constant c such that r′r is labelled with ⟨q,c⟩ q_ C,c , q↝−q∈(ℛ,(c))q_ B _ R^-q_ C (R, C(c)), and (c,b)∈ℱ R(c,b) . This case is analogous to the previous one. • Consider the root r and its multiple children r1,…,rnr_1,…,r_n. By Definition˜3, there are some 1,…,n∈ C_1,…, C_n∈ Classes such that r1r_1 is labelled with ⟨q1,b⟩ q_ C_1,b , r2r_2 with ⟨q2,b⟩ q_ C_2,b , and so on. Moreover, q↝εq1,…,qnq_ B _ \q_ C_1,…,q_ C_n\ in (γ)DLA(γ). Now, for every 1≤i≤n1≤ i≤ n, consider the subtree ⟨Ni,Ei,Li⟩ N_i,E_i,L_i of ⟨N,E,L⟩ N,E,L rooted at rir_i, which is of height at most k−1k-1 and is an accepting run of (γ)DLA(γ) over ℱF from ⟨qi,b⟩ q_ C_i,b . From the existence of this trees, we conclude that 1(b),…,n(b)∈(ℛ,ℱ) C_1(b),…, C_n(b) (R,F) by induction hypothesis. Therefore, (b)∈(ℛ,ℱ) B(b) (R,F) since 1(x)∧…∧n(x)→(x)∈ℛ C_1(x) … C_n(x)→ B(x) . In either case above, we have (b)∈(ℛ,ℱ) B(b) (R,F). Appendix 0.C Proofs of Section˜5 In this section, we provide complete proofs of the results from Section˜5. More precisely, we prove Lemmas 7, 7, and 8. Note that Example˜8 follows directly as a corollary of the latter two lemmas. * Proof We first prove the forward implication of the equivalence stated in the lemma. Assume that there is an accepting run of N on ℱF starting from ⟨q,s⟩ q,s , and let n1,…,nkn_1,…,n_k be the sequence of nodes occurring, in order, along the unique branch of this run. Note that k≥2k≥ 2 since q is different from the accepting state. Then we are in one of the following cases: • If k=2k=2, then either q↝εqacc∈q _ \q_acc\∈ N or, otherwise, q↝qacc∈q _ C\q_acc\∈ N for some ∈ C∈ Classes. In the first case, the disjunct ⊤ is in NFA(,q,s)PQ_NFA( N,q,s), and that disjunct is entailed by ℱF. In the second case, the disjunct (s) C(s) is in NFA(,q,s)PQ_NFA( N,q,s), and that disjunct is entailed by ℱF since (s)∈ℱ C(s) . Note that this fact is in ℱF because the run is accepting and q↝εqacc∉q _ \q_acc\∉ N. • If k≥3k≥ 3, then consider the node nk−1n_k-1 and its label ⟨p,t⟩ p,t . Since the NFA can transition from ⟨q,s⟩ q,s to ⟨p,t⟩ p,t in ℱF, we have that ℱF entails q⊳p(s,t) E N_q p(s,t) from Lemma˜1. Now, one of the following cases must hold: – If p↝εqacc∈p _ \q_acc\∈ N, then the disjunct ∃x.q⊳p(s,x)∃ x. E N_q p(s,x) is in NFA(,q,s)PQ_NFA( N,q,s) and ℱF entails this disjunct, since this fact set entails q⊳p(s,t) E N_q p(s,t). – If not, then there is some ∈ C∈ Classes such that p↝qacc∈p _ Cq_acc∈ N, and, since the run is accepting, (t)∈ℱ C(t) . In this case, the disjunct ∃x.q⊳p(s,x)∧(x)∃ x. E N_q p(s,x) C(x) occurs in NFA(,q,s)PQ_NFA( N,q,s) and is entailed by ℱF. This is indeed the case since ℱF entails both q⊳p(s,t) E N_q p(s,t) and (t) C(t). In either case, we have that ℱF satisfies NFA(,q,s)PQ_NFA( N,q,s). For the reverse direction of the equivalence, assume that ℱF satisfies NFA(,q,s)PQ_NFA( N,q,s). Then ℱF satisfies at least one disjunct ψ of this PQ. Depending on the type of disjunct satisfied by ℱF, one of the following cases applies: • If ψ=⊤ψ= , then there is a transition q↝εqacc∈q _ \q_acc\∈ N. In that case, the run from ⟨q,s⟩ q,s to ⟨qacc,s⟩ q_acc,s is accepting for ℱF in N. • If ψ=(s)ψ= C(s) for some ∈ C∈ Classes, then we have q↝qacc∈q _ C\q_acc\∈ N. In that case, the run ℱF from ⟨q,s⟩ q,s to ⟨qacc,s⟩ q_acc,s is accepting since (s)∈ℱ C(s) . • Assume that ψ is of the form ∃w.q⊳p(s,w)∧(w)∃ w. E_q p N(s,w) C(w). Then, there is some constant t such that ℱF entails q⊳p(s,t) E_q p N(s,t) and (t) C(t), and p↝qacc∈p _ C\q_acc\∈ N. From Lemma˜1, we conclude that N can transition from ⟨q,s⟩ q,s to ⟨p,t⟩ p,t in ℱF, that is, that there is a run of N over ℱF that starts on a node labelled with ⟨q,s⟩ q,s and ends on a node labelled ⟨p,t⟩ p,t . If we append one more node at the end of this run labelled with ⟨qacc,t⟩ q_acc,t , we obtain an accepting run of N starting ⟨q,s⟩ q,s over ℱF; recall that p↝qacc∈p _ C\q_acc\∈ N and that (t)∈ℱ C(t) . • Assume that ψ is of the form ∃w.q⊳p(s,w)∃ w. E_q p N(s,w). Then, there is some constant t such that ℱF entails q⊳p(s,t) E_q p N(s,t), and p↝εqacc∈p _ \q_acc\∈ N. From Lemma˜1, we conclude that N can transition from ⟨q,s⟩ q,s to ⟨p,t⟩ p,t in ℱF, that is, that there is a run of N over ℱF that starts on a node labelled with ⟨q,s⟩ q,s and ends on a node labelled ⟨p,t⟩ p,t . If we append one more node at the end of this run labelled with ⟨qacc,t⟩ q_acc,t , we obtain an accepting run of N starting ⟨q,s⟩ q,s over ℱF; recall that p↝εqacc∈p _ \q_acc\∈ N. In any case, we have an accepting run for N from ⟨q,s⟩ q,s over ℱF. We then show a preliminary lemma allowing us to substitute an automaton A to its extended version: for the following, we will assume that A is in extended form. Lemma 6 Consider an automaton =⟨s,Q,qinit,δ⟩ A= s,Q,q_init,δ and its extended version ε=⟨s,Q,qinit,δ∪δε∗⟩ A_ = s,Q,q_init,δ∪ _ ^* . For every fact set ℱF, state p∈Qp∈ Q, and constant c, there is an accepting run of A over ℱF from ⟨c,p⟩ c,p if and only if there is an accepting run of ε A_ over ℱF from ⟨c,p⟩ c,p . Therefore, A and ε A_ are equivalent. Proof The inclusion of A in ε A_ is trivial. For the other direction, we show that every ε - transition of ε A_ can be simulated by a finite sequence of ε -transitions in δ: from this, it follows that if there is an accepting run on ε A_ for some fact set ℱF, starting node ⟨p,c⟩ p,c then there is an accepting run on A for the same fact set and starting node. First note that we can express δε∗ _ ^* as the (finite) limit of some δ0,…,δn,… _0,…, _n,… defined such that δ0=q↝εq∣q∈Q _0=\q _ q q∈ Q\ and for every i≥0i≥ 0, δi+1=δi∪q↝ε(P∖p)∪P′∣q∈Q _i+1= _i∪\q _ (P \p\)∪ P q∈ Q\ where p is a state, and P and P′P are sets of states such that q↝εP∈δiq _ P∈ _i, and p↝εP′∈δp _ P ∈δ, and p∈Pp∈ P. We then show, by induction on i, that every δi _i can be simulated by a finite sequence of transitions of δ. For the base case, if the transition is of form q↝εqq _ \q\, then the transition can be simulated by an empty sequence of transitions: therefore δ0 _0 can be simulated by a finite sequence of transitions of δ. For the induction step, we assume that δi⊆δε∗ _i _ ^*, and consider δi+1=δi∪q↝εQ′ _i+1= _i∪\q _ Q \. Then there are some P, p, P′P so that q↝εP∈δiq _ P∈ _i, and p∈Pp∈ P, and p↝εP′∈δp _ P ∈δ, and Q′=(P∖p)∪P′Q =(P \p\)∪ P . Since q↝εP∈δiq _ P∈ _i, it can be simulated by a finite sequence t1,…,tnt_1,…,t_n of transitions in δ. Then, the sequence of transitions t1,…,tn,p↝εP′t_1,…,t_n,p _ P simulates q↝εQ′q _ Q : indeed, the transition p↝εP′p _ P can be added to the sequence since p∈Pp∈ P. Doing so removes p and adds P′P to the states at the end of the sequence: therefore, the states at the end of the new sequence are (P∖p)∪P′=Q′(P \p\)∪ P =Q . Therefore we can simulate δi+1 _i+1 with a finite sequence of transitions of δ. We then move on to the two main lemmas. Lemma 7 A stratified DL automaton A contains ()PQ( A). Proof We fix a stratified DL automaton =⟨s,Q,qinit,δ⟩ A= s,Q,q_init,δ , its extended version ε=⟨s,Q,qinit,δ∪δε∗⟩ A_ = s,Q,q_init,δ∪ _ ^* , the query ()PQ( A), and a fact set ℱF. To prove the lemma, we assume that ℱF entails ()PQ( A) and show that ε A_ accepts ℱF. More precisely, we prove the following claim by induction on k≥1k≥ 1: if ℱF entails (,p,c)PQ( A,p,c) for some state p of A in stratum k and some constant c, then there is an accepting run of ε A_ on ℱF starting from ⟨p,c⟩ p,c . Applying this claim to p=qinitp=q_init and c=sc=s, we obtain an accepting run of ε A_ on ℱF starting from ⟨qinit,s⟩ q_init,s , and hence ε A_ accepts ℱF. Recall that A and ε A_ are equivalent by Lemma˜6 and therefore, the lemma follows. For the base case, let p be a state in stratum 11 and c a constant such that ℱF satisfies (,p,c)PQ( A,p,c). Since p belongs to stratum 11, no state succeeds p with respect to ≻ _ A. Therefore, by Definition˜10, we have: (,p,c)=⋁p↝εP∈δε∗⋀q∈PNFA((,p),q,c)PQ( A,p,c)= _p _ P∈δ^*_ _q∈ PPQ_NFA(NFA( A,p),q,c) Since this PQ is entailed by ℱF, there is some p↝εq1,…,qm∈δε∗p _ \q_1,…,q_m\∈δ^*_ such that ℱF satisfies ⋀1≤i≤mNFA((,p),qi,c) _1≤ i≤ mPQ_NFA(NFA( A,p),q_i,c). Since this formula is a conjunction, ℱF satisfies NFA((,p),qi,c)PQ_NFA(NFA( A,p),q_i,c) for every 1≤i≤m1≤ i≤ m. Hence, there is an accepting run for A over ℱF from every ⟨qi,c⟩ q_i,c by Definition˜7. Therefore, for every 1≤i≤m1≤ i≤ m, there is an accepting run ⟨Ni,Ei,Li⟩ N_i,E_i,L_i for ε A_ over ℱF from ⟨qi,c⟩ q_i,c by Lemma˜6. Without loss of generality, we assume that the sets N1,…,NmN_1,…,N_m are mutually disjoint. Now, consider the tree ⟨N,E,L⟩ N,E,L defined as follows: • Let N=N1∪…∪Nm∪rN=N_1∪…∪ N_m∪\r\ with r a fresh node that is the root of this tree. • Let E=E1∪…∪Em∪r→r1,…,r→rmE=E_1∪…∪ E_m∪\r→ r_1,…,r→ r_m\ with r1r_1 the root of ⟨N1,E1,L1⟩ N_1,E_1,L_1 , r2r_2 the root of ⟨N2,E2,L2⟩ N_2,E_2,L_2 , and so on. • Let L be the mapping extending LiL_i for every 1≤i≤m1≤ i≤ m and maps r to ⟨p,c⟩ p,c . We argue that ⟨N,E,L⟩ N,E,L is an accepting run for ε A_ over ℱF from ⟨p,c⟩ p,c . This follows because p↝εq1,…,qm∈δε∗p _ \q_1,…,q_m\∈δ^*_ and hence, the edges r→r1,…,r→rm\r→ r_1,…,r→ r_m\ in this tree satisfy Definition˜3. Moreover, for every 1≤i≤m1≤ i≤ m, we have that ⟨Ni,Ei,Li⟩ N_i,E_i,L_i is an accepting run over ℱF from ⟨qi,c⟩ q_i,c . Hence, all of the edges in E1∪…∪EmE_1∪…∪ E_m also satisfy this definition, and all of the leaves in ⟨N,E,L⟩ N,E,L feature the accepting state. For the induction step, we consider a state p of stratum k≥2k≥ 2 and a constant c such that ℱF satisfies (,p,c)PQ( A,p,c). Since ℱF satisfies (,p,c)PQ( A,p,c), it satisfies some disjunct, there is some p↝εq1,…,qm∈δε∗p _ \q_1,…,q_m\∈ _ ^* such that ℱF satisfies the following: ⋀1≤i≤m(NFA((,p),qi,c) _1≤ i≤ m (PQ_NFA(NFA( A,p),q_i,c) ⋁∀p′,p1,…,pn∈Q such that qi→∗p′,p′↝εp1,…,pn,qi≻p1,…,qi≻pn(∃w.qi⊳p′(c,w)⋀1≤j≤n(,pj,w))) _ subarrayc∀ p ,p_1,…,p_n∈ Q such that q_i _ N^*p ,\\ p _ \p_1,…,p_n\,~q_i _ Ap_1,…,q_i _ Ap_n subarray (∃ w. E_q_i p N(c,w) _1≤ j≤ nPQ( A,p_j,w) ) ) In the remainder of our argument, we define an accepting run ⟨N,E,L⟩ N,E,L for ε A_ over ℱF from ⟨p,c⟩ p,c . The root node r∈Nr∈ N of this run is mapped by L to ⟨p,c⟩ p,c . Moreover, there are some distinct nodes r1,…,rm∈Nr_1,…,r_m∈ N such that, for every 1≤i≤m1≤ i≤ m, we have that r→ri∈Er→ r_i∈ E and L(ri)=⟨qi,c⟩L(r_i)= q_i,c . Now, for every 1≤i≤m1≤ i≤ m, we extend the run ⟨N,E,L⟩ N,E,L in the following manner: • If ℱ⊧NFA((,p),qi,c)F _NFA(NFA( A,p),q_i,c), there is an accepting run on A over ℱF from ⟨qi,c⟩ q_i,c as argued in the base case. We attach this directed tree to the node rir_i. • Otherwise, there is a constant t and some states p′,p1,…,pn∈Qp ,p_1,…,p_n∈ Q such that q→∗p′q _ N^*p , p′↝εp1,…pnp _ \p_1,… p_n\, q≻p1q _ Ap_1, …, q≻pnq _ Ap_n, and ℱF satisfies the following PQ: qi⊳p′(c,t)∧⋀1≤i≤n(,pi,t) E_q_i p N(c,t) _1≤ i≤ nPQ( A,p_i,t) Since ℱF satisfies qi⊳p′(c,t) E_q_i p N(c,t), we have from Lemma˜1 that there is a run whose root node is labeled ⟨qi,c⟩ q_i,c and whose unique leaf is labeled ⟨p′,t⟩ p ,t : we attach this directed tree to rir_i, and call the fresh leaf node ri′r_i . Since ℱF satisfies p′↝εp1,…,pnp _ \p_1,…,p_n\, the edge ⟨p′,t⟩→⟨pj,t⟩∣j≤n p ,t →\ p_j,t j≤ n\ is valid: we attach it to ri′r_i , and label the fresh leaves nodes ri,j′r _i,j. Since ℱF satisfies (,p1,t)PQ( A,p_1,t),…, (,pn,t)PQ( A,p_n,t), by induction hypothesis, there are accepting runs ⟨Nj′,Ej′,Lj′⟩ N _j,E _j,L _j from ⟨p1,t⟩ p_1,t , …, ⟨pn,t⟩ p_n,t . We attach each ⟨Nj′,Ej′,Lj′⟩ N _j,E _j,L _j to ri,j′r _i,j. After the modifications, ⟨N,E,L⟩ N,E,L has only accepting leaves: we have built an accepting run for A over ℱF from ⟨p,c⟩ p,c . We conclude that there is an accepting run of A over ℱF from ⟨p,c⟩ p,c , and the induction step holds. Therefore, if some ℱF satisfies the PQ φ() ( A), we have an accepting run of A from ⟨qinit,s⟩ q_init,s over ℱF. Lemma 8 A DL automaton A is contained in ()PQ( A). Proof We fix a DL automaton =⟨s,Q,qinit,δ⟩ A= s,Q,q_init,δ and a fact set ℱF. To prove the lemma, we assume that there is an accepting run of A from ⟨qinit,s⟩ q_init,s over ℱF, and show that this implies that ℱF satisfies (,qinit,s)PQ( A,q_init,s). More precisely, we show the following claim by induction on k≥1k≥ 1: for any state p of A in stratum k and any constant c, if A has an accepting run from some ⟨p,c⟩ p,c we have ℱ⊧(,p,c)F ( A,p,c). Applying this claim to qinitq_init and s, it follows that if there is an accepting run for ℱF from ⟨qinit,s⟩ q_init,s , then ℱF satisfies (,qinit,s)PQ( A,q_init,s). For the base case, consider a state p of stratum 1 and an accepting run ⟨N,E,L⟩ N,E,L whose root is labeled ⟨p,c⟩ p,c and whose leaves are labeled with ⟨qacc,w1⟩,…,⟨qacc,wn⟩\ q_acc,w_1 ,…, q_acc,w_n \ for some w1,…,wnw_1,…,w_n in A. We define the epsilon-section of ⟨N,E,L⟩ N,E,L , noted ⟨N,E,L⟩ε N,E,L _ , as the (maximal) subset run starting from the root using only edges matched with ε -transitions. By the definition of δε∗ _ ^*, there is a transition p↝εQ′∈δε∗p _ Q ∈ _ ^* such that the leaves of ⟨N,E,L⟩ε N,E,L _ are labeled with the states of Q′Q . Since p is of stratum 1, there can be only binary edges below these nodes: if that was not the case, some states of leaves of the run would be of a lower strata than the state of the root. Moreover, for every q∈Q′q∈ Q , there is an accepting run from ⟨q,c⟩ q,c in =(,p) N=NFA( A,p) over ℱF. By Definition˜7, this means that NFA(,q,c)PQ_NFA( N,q,c) accepts. Therefore, the PQ ⋁p↝εQ′⋀q∈Q′NFA(,q,c)=(,qinit,c) _p _ Q _q∈ Q PQ_NFA( N,q,c)=PQ( A,q_init,c) accepts and the property is verified. For the induction step, if p is of strata k≥2k≥ 2, we consider an accepting run for ⟨p,c⟩ p,c on A. Similarly to the base case, we consider the epsilon-section of the run: if there are only binary edges outside of it, then we are in the same situation as in the base case. If not, we consider the leaves r1,…,rmr_1,…,r_m of the epsilon-section of the run, labeled ⟨qi,c⟩∣i≤m\ q_i,c i≤ m\. For each i, we are in one of two cases: • If rir_i has only binary edges descending from it, then the part of the tree rooted at rir_i is an accepting run for (,q)NFA( A,q). In that case, NFA((,p),qi,c)PQ_NFA(NFA( A,p),q_i,c) is satisfied. • If that is not the case, consider the first multi-ary edge descending from rir_i, called ri′→ri,1′,…,ri,n′r _i→\r _i,1,…,r _i,n\ with ri′r _i labeled ⟨p′,t⟩ p ,t and each ri,j′r _i,j labeled ⟨pj,t⟩ p_j,t . – By definition, ⟨q,c⟩ q,c can transition to ⟨p′,t⟩ p ,t in =(,q) N=NFA( A,q): therefore, by Lemma˜1 we have ∃w.q⊳p′(c,t)∃ w. E_q p N(c,t). – Moreover, in the automaton, we have that p′↝εp1,…,pnp _ \p_1,…,p_n\, and since p1p_1 , …, and pnp_n follow a multi-ary transition outside the epsilon-section of the run qi≻p1q_i _ Ap_1, …, and qi≻pnq_i _ Ap_n. – Since the run is accepting, the sub-runs starting at ri,1′r _i,1, …, ri,n′r _i,n are valid runs with only accepting leaves: they are also accepting for A over ℱF. As p1,…,pnp_1,…,p_n have strata at most k, by induction hypothesis, ⋀1≤j≤n(,pj,t) _1≤ j≤ nPQ( A,p_j,t) is satisfied by ℱF. It follows that ⋀i≤m(NFA(,qi,t)∨ _i≤ m (PQ_NFA( N,q_i,t)~ ⋁∀p′,p1,…,pn∈Q such that qi→∗p′,p′↝εp1,…,pn,qi≻p1,…, and qi≻pn(∃w.qi⊳p′(t,w)∧⋀1≤j≤n(,pj,w))) _ subarrayc∀ p ,p_1,…,p_n∈ Q such that q_i _ N^*p ,\\ p _ \p_1,…,p_n\,~q_i _ Ap_1,…, and q_i _ Ap_n subarray (∃ w. E_q_i p N(t,w) _1≤ j≤ nPQ( A,p_j,w) ) ) is satisfied for some Q, and therefore that (,p,c)PQ( A,p,c) is. Therefore, we have that for any state p and constant c, if there is an accepting run of A from ⟨p,c⟩ p,c over ℱF, then ℱF satisfies (,p,c)PQ( A,p,c). Appendix 0.D Claim of Section˜7 We provide more details regarding our claim that positive fragments of DL-Litecore and DL-LiteR sets of rules always have stratified associate DL automata. We assume familiarity with DL-Lite and refer the reader to [5]; we discuss positive DL-LiteR since it subsumes DL-Litecore. Let us first highlight that, to be seen as Horn-ℒℋℐHorn-ALCHI rules in our normal form, positive DL-LiteR rules requires the introduction of a placeholder class ⊤ C_ that replaces ⊤ in every occurrence of a DL-Lite concept of form ∃.⊤∃ R. (or, as is common, simply ∃ R), where R is possibly an inverse role. We add the rule →⊤(x)→ C_ (x) (axiom of form (4)) to witness this behavior. Let us now examine the normalization exposed in Section˜3. Getting rid of axioms of form (6) and (7) does not introduce any axiom of form (1) with n≥2n≥ 2, as desired. In Appendix˜0.A, we already established that inference rules Rules ≤R_≤, ≤−R^-_≤, ⊑rR^r_ and ⊥R_ never apply. Therefore, the only inference rule in [10, Table 2] that may introduce axioms of form (1) with n≥2n≥ 2 is the rule ∀R_∀. To apply, this rule requires an axiom with shape ⊑∀. A ∀ R. B. However, none of the other rules may produce such axiom, therefore it must come directly from our DL-LiteR rules. This implies that =⊤ A= C_ . The body of the inferred rule thus, syntactically, takes the form (1) with n≥2n≥ 2. However, due to our rule →⊤(x)→ C_ (x), it is equivalent to the exact same inferred rule, but in which every occurrence of ⊤ C_ has been removed from its body, which restores n≤1n≤ 1.