--- title: "Rewriting the Description Logic ALCHIQ to Disjunctive Existential Rules" authors: - "David Carral" - "Markus Krötzsch" doi: "10.24963/ijcai.2020/246" url: "https://ijcai.org/proceedings/2020/246" pdf: "https://ijcai.org/proceedings/2020/0246.pdf" venue: "Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence" year: 2020 pages: "1777-1783" track: "Main track" keywords: - "Knowledge Representation and Reasoning: Description Logics and Ontologies" - "Knowledge Representation and Reasoning: Logics for Knowledge Representation" - "Knowledge Representation and Reasoning: Knowledge Representation Languages" --- # Rewriting the Description Logic ALCHIQ to Disjunctive Existential Rules David Carral, Markus Krötzsch *Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence*, pages 1777-1783. DOI: [10.24963/ijcai.2020/246](https://doi.org/10.24963/ijcai.2020/246) ## Abstract Especially in data-intensive settings, a promising reasoning approach for description logics (DLs) is to rewrite DL theories into sets of rules. Although many such approaches have been considered in the literature, there are still various relevant DLs for which no small rewriting (of polynomial size) is known. We therefore develop small rewritings for the DL \ALCHIQ -- featuring disjunction, number restrictions, and inverse roles -- to disjunctive Datalog. By admitting existential quantifiers in rule heads, we can improve this result to yield only rules of bounded size, a property that is common to all rewritings that were implemented in practice so far. ## Full text ## 1 Introduction Among the many approaches towards efficient reasoning in description logics (DLs), consequence-preserving translations of DL theories into rule languages are among the most prominent. Table 1 gives an overview of works in this area. The natural strength of rule reasoners is their good scalability towards large sets of facts. Indeed, all of the rewritings in Table 1 are independent of the given facts (ABox), which can be used unchanged for reasoning with the rule-based theory. In general, we can describe this idea of rewriting as follows: Definition 1. Consider fragments L1 and L2 of first-order logic that include ground facts. An L2-theory T2 is a fact-entailment preserving rewriting (or simply rewriting in this paper) of an L1-theory T1 if, for every set F of ground facts and every ground fact ϕ over the signature of T1, we have T1, F |= ϕ iff T2, F |= ϕ. If such a rewriting can always be computed, then L1 is (effectively, fact-entailment preserving) rewritable to L2. All of the works in Table 1 establish rewritability in this sense for the given fragments, and in particular preserve entailments of all role (i.e., binary) atoms. If only entailments of class (i.e., unary) atoms are of interest, then all uses of ALC in the table can also be replaced by S - and by SR at the cost of exponentially larger rewritings - based on common preprocessing techniques [Ortiz et al., 2010]. Entailment of (complex) role atoms is also a special case of regular path | Work | Source | Target | Size | |-------------------------------------------------------------------------------------------------------------|---------------------------------------|----------------------------------------------------|------------------------------------| | Hustadt et al. [2007] Eiter et al. [2012] Rudolph et al. [2012] Bienvenu et al. [2014] Carral et al. [2018] | ALCHIQ Horn-SHIQ SHIQbs SHI Horn-SHIQ | Datalog∨ Datalog Datalog∨ Datalog∨ Datalog Datalog | exp. † exp. † exp. † exp. † exp. † | | | Horn-ALCHOIQ | | | | Carral et al. [2019b] | | | exp. † | | | Horn-SRIQ | Datalog | 2exp.† | | Ortiz et al. [2010] Ahmetaj et al. [2016] Kr¨otzsch [2011] | Horn-ALCHOIQ | Datalog | poly. | | | ALCHIO | Datalog∨ | poly. | | | EL++ | Datalog | poly.† | | Carral et al. [2019a] | Horn-ALC | Datalog∃ | poly.† | †: rules of bounded size that does not depend on input Table 1: Rewritings of DL-type logics to rule languages, where Datalog∨ and Datalog∃ denote Datalog extended with disjunctions and existential quantifiers, respectively query answering, which can be solved by combined methods that we do not discuss here [Simancik, 2012]. While the works in Table 1 rely on diverse rewriting methods, they must all obey some complexity-related constraints. In particular, if L1 is rewritable to L2, then L2's data complexity for fact entailment subsumes that of L1. Hence, HornDLs (P-complete in data) are rewritable to Datalog, while non-Horn DLs (co-NP-complete in data) supposedly are not. Combined complexity is also a limiting factor. It is EXPTIME-complete for Datalog and co-NEXPTIME-complete for Datalog∨, but drops to P and NP, respectively, if rule sizes are bounded († in Table 1). This explains why †-rewritings from (N)EXPTIME-complete DLs to Datalog(∨) must produce exponentially large rule sets. The alternative is to allow polynomially growing rule sizes (and especially predicate arities). The last two lines in Table 1 are rewritings that use a constant rule sets and rewrite TBoxes to facts in (sub)polynomial time. This works for EL++ due to its P-complexity, and for Horn-ALC due to the high expressive power of Datalog∃ theories, even when these are constant. Given this rich body of research in rule rewritings, there is a surprising shortage of rewriting-based reasoners. KAON2 uses the exponential SHIQ rewriting of Hustadt et al. [2007], and DReW the polynomial EL++ rewriting of Kr¨otzsch [2011] - both systems are discontinued. Rule reasoners, in contrast, have been thriving in recent years, and scalable systems exist both for Datalog∨ (e.g., answer set programming engines [Lifschitz, 2019]) and for Datalog∃ (e.g., engines for tuple-generating dependencies [Bellomarini et al., 2018; Motik et al., 2014; Urbani et al., 2018]). A possible explanation is that known rewritings still suffer from many shortcomings. Indeed, exponentially large rule sets (Table 1, lines 1-7) and rule sizes in the order of the ontology (lines 8-9) both impair practical performance, whereas static rewritings (lines 10-11) are often better implemented in dedicated "consequence-based" reasoners rather than relying on general-purpose rule reasoners [Kazakov et al., 2013]. Moreover, Table 1 highlights that many DL feature combinations are not supported by any polynomial rewriting. In this paper, we therefore study polynomial rewritings for hitherto unsupported DLs, in particular for the combination of number restrictions (Q) and inverses (I) on a non-Horn DL. The result are two new rewriting approaches for the DL ALCHIQ: a rewriting to Datalog∨ that (unavoidably) requires unbounded (but still linear) rule sizes, and a rewriting to Datalog∨∃ that achieves bounded rule sizes. Datalog with existential quantifiers is co-re-complete for fact entailment, but we show that our rewriting leads to rule sets for which entailment can be decided with standard algorithms, while still matching the original DL's co-NP data complexity. Both results are new, and - in the second case - also illustrate the potential advantage of considering rules with existential quantifiers as a target for rewriting. Finally, we also consider Horn-ALCHIQ, the disjunctionfree fragment of ALCHIQ. Whereas our rewriting of ALCHIQ to Datalog∨ and Datalog∨∃ , respectively, could be applied here, it produces rule sets that always contain disjunctions. We therefore combine several known results to obtain alternative, disjunction-free rewritings for this case. After acceptance, some proofs were moved to a technical report [Carral and Kr¨otzsch, 2020], following reviewers' suggestions to include additional explanations instead. ## 2 Preliminaries We introduce Datalog∨∃ as a first-order rule language, and define Datalog, Datalog∨, and the DL ALCHIQ as fragments thereof. The datalog-first disjunctive chase provides a suitable deduction calculus for the Datalog∨∃ fragments we rewrite to. We assume familiarity with standard notions of first-order logic, such as interpretations and homomorphisms. ## 2.1 Rules and Logic Fragments We consider a first-order signature based on mutually disjoint, countably infinite sets of constants C, variables V, nulls N, and predicates P. The set of terms is T = C ∪ V ∪ N. A predicate P ∈ P has an arity ar(P) ≥ 1, Pi = {P | ar(P) = i}. We consider special predicates ⊤,⊥ ∈ P1 , and ≈ ∈ P2 , which are semantically interpreted as universal class, empty class, and equality. For a logical expression or set thereof υ and a set of entities E ∈ {C,V,N,T,P} ∪ {Pi | i ≥ 1}, let Eυ be the set containing every element in E that occurs in υ. Lists of terms t1, . . . , tn are written as ⃗t and treated as sets when order is irrelevant. Letters x, y, z, w, and v, possibly with subscripts, always denote variables. Figure 1: ALCHIQ rules (A, B, C ∈ P1 and R, S, V ∈ P2 \{≈}) | ( C⊓) | A(x) ∧B(x) →C(x) A⊓B ⊑ C | |-----------------------------------|----------------------------| | ( C⊔) A(x) →B(x) ∨C(x) | A ⊑ B ⊔C | | ( ∀ ) A(x) ∧R(x, y) →B(y) | A ⊑ ∀R.B | | ( ∃ ) A(x) → ∃y.R(x, y) ∧B(y) | A ⊑ ∃R.B | | (◦) A(x) ∧R(x, y) ∧B(y) →S(x, y) | A ◦ R ◦ B ⊑ S | | (⩽) R(x, y) ∧R(x, z) → y ≈ z | ⊤ ⊑ ⩽1R.⊤ | | ( R⊓) R(x, y) ∧S(x, y) → V (x, y) | R⊓S ⊑ V | | ( R⊔) R(x, y) →S(x, y) ∨ V (x, y) | R ⊑ S ⊔ V | | (-) R(y, x) → S(x, y) | R- ⊑ S | An atom is a formula P(⃗t) with P ∈ P|⃗t| and ⃗t ⊆ T. A fact is a variable-free atom. A disjunctive existential rule is a null-free first-order logic formula of the form where β[⃗x] and ηi[⃗xi, ⃗yi] are conjunctions of atoms using variables in the specified lists ⃗x(i) and ⃗yi, which satisfy ⃗xi ⊆ ⃗x and ⃗x ∩ ⃗yi = ∅ for all 1 ≤ i ≤ n. The rule has body β[⃗x] and head ∨ni=1 ∃⃗yi.ηi[⃗xi, ⃗yi]. We omit the universal quantifiers when writing rules. We use disjunctions in bodies as a shortcut, e.g., we write β1 ∨ β2 → ∃⃗y.η instead of β1 → ∃⃗y.η and β2 → ∃⃗y.η. Definition 2. Datalog∨∃ is the language of all sets R of disjunctive existential rules. We consider some of its fragments: - Datalog∃ : Datalog∨∃ without disjunction. - Datalog∨: Datalog∨∃ without existential quantifiers. - Datalog: Datalog∨ without disjunctions. - ALCHIQ: rules of one of the forms given in Figure 1. - Horn-ALCHIQ: ALCHIQwithout disjunction. Our definition of ALCHIQ is based on first-order representations of the axioms of the DL SHIQbs shown on the right of Figure 1. Arbitrary ALCHIQ axioms [Horrocks et al., 2000] can be converted into these forms while preserving entailment of facts [Rudolph et al., 2012, Section 6]. Note that this conversion can be computed in polynomial time if the number restrictions are encoded in unary. An ontology O is a pair 〈R, F〉 of a rule set R and a nullfree fact set F. Without loss of generality, we assume PF ⊆ PR and ⊤,⊥,≈ /∈ PF. We write O |= υ if O entails a logical expression υ in first-order logic with ≈, ⊤, and ⊥. ## 2.2 The Chase. We introduce a general proof procedure for Datalog∨∃ as the non-deterministic version of the restricted chase algorithm. Following Carral et al. [2019a], we prioritise Datalog∨ rules to increase the chance of termination. A substitution is a partial function σ : V → C∪N. For a logical expression υ, let υσ be the result of replacing each variable x in υ by σ(x) if the latter is defined. Given a fact set F and a rule ρ of the form (‡), σ is a match for ρ if it is not defined on ⃗y1 ∪ . . . ∪ ⃗yn and βσ ⊆ F. Definition 3. A chase sequence of an ontology 〈R,F〉 is a (finite or infinite) sequence of fact sets F0, F1, . . . such that 1. F0 = F; 2. for every Fi+1 with i ≥ 0, there is a rule ρ ∈ R of the form (‡) and a match σ for ρ on Fi such that 3. (a) Fi ̸|= ∃⃗yi.ηiσ for all i ∈ {1, . . . , n}, 4. (b) Fi+1 = Fi ∪ ηj ˆσ for some j ∈ {1, . . . , n}, where ˆσ extends σ to ⃗yj such that ˆσ(y) ∈ N is a fresh null for each y ∈ ⃗yj , 5. (c) if ρ contains an existential quantifier, then for all Datalog∨ rules ρ′ ∈ R and all matches σ′ of ρ′ on Fi, we have Fi |= ρ′σ′ (priority for Datalog∨); 3. for every ρ ∈ R and substitution σ, there is some k ≥ 1 such that Fi |= ρσ for all i ≥ k (fairness). The chase process is non-deterministic in several ways. Disjunctions are handled by the choice of j in (2b). This affects which facts are derived. Another form of nondeterminism is in the choice of rule application order, within the constraints of (2c) and (3). This does not affect which ground facts are eventually derived, but it may determine if the chase sequence is finite or not. A rule set R is (universally) terminating if, for all fact sets F, all chase sequences of 〈R, F〉 are finite. The language of all terminating rules sets is called terminating Datalog∨∃ (and similarly for other logics). Definition 3 does not consider the semantics of the special predicates ⊤, ⊥, and ≈, which must satisfy certain restrictions in all first-order interpretations: ⊤ and ⊥ are interpreted as the domain and the empty set, respectively, and ≈ is used to denote equality. We treat these special predicates by axiomatisation. For a rule ρ, let Ax(ρ) be the result of replacing all occurrences of ⊤, ⊥, and ≈ by Top, Bot, and Eq, respectively. For a rule set R, let Ax(R) be the rule set that contains (i) Ax(ρ) for all ρ ∈ R, (ii) Top(c) for all c ∈ CR, and (iii) the following rules instantiated for all P ∈ PR \ {⊤, ⊥, ≈} and i ∈ {1, . . . , n}: The rules are clearly sound for the intended interpretation of the auxiliary predicates. The second rule type ensures that everything follows from a contradiction - practical systems would omit this for reasons of efficiency, and check for entailments over Bot as a special case. The final three rules are the usual equality theory, where we omit reflexivity since it does not lead to conclusions for any predicates other than Eq. Fact 1. An ontology O = 〈R, F〉 entails a fact ϕ over a predicate in PO \ {⊤, ⊥, ≈} iff ϕ is in all chases of 〈Ax(R), F〉. ## 3 ALCHIQ to Disjunctive Datalog We will now specify a polynomial rewriting of ALCHIQ to Datalog∨, and establish its correctness. For the remainder of this section, let R be an arbitrary, fixed ALCHIQ rule set. Moreover, let R∃ be the set of all rules of type (∃) in R; that is, the set of all non-Datalog rules in R. We present a rewriting to establish the following main result. Figure 2: Sketch of the local environments as described by generic types (Type, left) and types for named elements x (NamType, right) ![Image](https://ijcai.org/proceedings/2020/fulltext/246/image_000000_77373f5e3b9e2f9882b99386802adf946047633b172dbcec9e202bc13fe4346f.png) Theorem 2. ALCHIQ is poly-time rewritable to Datalog∨. Our rewriting is based on types that define (shapes of) local environments of domain elements in a DL interpretation. Sketches for the intuitive notions of "local environment" that we consider are shown in Figure 2. The types abstract from pairs of elements c and d that are directly related, by specifying the classes of c, the classes of d, and the set of (forward or inverse) roles relating them. To support ALCHIQ, the type further considers, for each rule ρ ∈ R∃, a successor wρ of d that witnesses the satisfaction of ρ on d. This successor is again described by the (forward or inverse) roles between d and wρ, and by the classes of wρ. A type therefore is a tuple 〈C,R,D, S1,E1, . . . , Sℓ,Eℓ〉 where ℓ = |R∃|, C, D, Ei ⊆ P1 , and R, Si ⊆ P2 \ {≈} for i ∈ {1, . . . , ℓ}. We encode types in Datalog∨ using a predicate Type of arity (2+ℓ)·|P1R ∪{⊤, ⊥}|+(1+ℓ)·2|P2R \{≈}|, where each parameter can be one of the fresh individuals {0, 1}, indicating the presence or absence of an element in one of the sets that constitute the type. This approach follows Ortiz et al. [2010]. We use the following fixed lists of variables in Type atoms: for some fixed orderings P1R ∪ {⊤,⊥} = {A1, . . . ,An}, P2R \ {≈} = {R1, . . . ,Rm}, and R∃ = {ρ1, . . . , ρℓ}; and with ⃗W ρ = wρR1 ,wρR1 . . . , wρRm , wρR-m , wρA1 , . . . , wρAn for every ρ ∈ R∃. We will frequently encounter atoms Type(⃗C, ⃗R, ⃗D, ⃗W), which we further abbreviate as Type(⃗V ). We will further use facts of the form NamType(x, ⃗D, ⃗W) to encode the type of a named individual x, specified by its classes ( ⃗D) and R∃ witnesses ( ⃗W). Definition 4. Let rew∨(R) be the Datalog∨ rule set that contains (i) Ax(R \ R∃); (ii) the rule set in Figure 3; and (iii), for every rule ρ ∈ R, the corresponding rules in Figure 4. In this rewriting, the rules of (i) are (axiomatised) firstorder versions of all non-existential ontology axioms. However, these rules will only apply to named individuals, since models of the rewritten Datalog∨ rules do not contain domain elements to represent the anonymous individuals that are relevant in DL models. Such anonymous elements instead are represented indirectly by recording their types, which is accomplished by rules (ii) and (iii). Rules (1) and (2) trigger Figure 3: Part of the Datalog∨ rewriting rew∨ (R) of ALCHIQ rule set R; [x1/a1, . . . , xn/an] is the substitution that maps every xi to ai Figure 4: Rewriting ALCHIQ rules ρ to Datalog∨ ; [x1/a1, . . . , xn/an] is the substitution that maps every xi to ai the construction of types by requiring that named individuals have types (1), and that existing types have compatible successor types that satisfy existential restrictions (2). All other rules in Figures 3 and 4 then restrict these types by excluding contradicting cases. Rule (3) ensures the consistent assignment of classes to named individuals, rule (4) excludes some basic inconsistencies, and rule (5) ensures that the second element ("d") of any type must satisfy ⊤ if it satisfies anything at all. We do allow the case where all bits for ⃗R and ⃗D are 0, which occurs, e.g., for named individuals without successors. Rules in Figure 4 encode the meaning of specific axioms when applied to the local structure of types as sketched in Figure 2. Most rules are straightforward, but the rules (⩽) for expressing functionality require some explanation. Note that these rules are instantiated for various combinations of existential restrictions, class names, and role names. The rules in the first line encode equality of two existential successors (illustrated by elements in classes ⃗Ei in Figure 2); the rules in the second line encode equality of an existential successor and the first element of the type (illustrated by the element in classes ⃗C in Figure 2). Using Eq in these lines ensures that bits that encode the equated elements' type data are identical, since equality of 0 and 1 is disallowed by (4). The rules in the last two lines capture cases where predicates of named individuals can be derived from predicates of successor elements (represented by bits in a type). Note that we cannot use Eq for achieving the latter. Equality of several named individuals is already supported by the corresponding axiom in Ax(R\R∃). For better clarity, we have chosen a presentation of rew∨(R) that is not polynomial, since rules (1) and (2) are of exponential size. To define a polynomial rewriting, we can simply substitute rule (1) with the rules where k = |⃗V |, the second rule is instantiated for all i = 1, . . . , k - 1, and ⃗xi is a list of variables of size i. We can replace the rules of type (2) in an analogous manner. To establish Theorem 2, it remains to proof soundness (Lemma 3) and completeness (Lemma 4). Lemma 3. For all fact sets F and all facts ϕ with a predicate in PR \ {⊤, ⊥, ≈}, if 〈R, F〉 ̸|= ϕ then 〈rew∨(R), F〉 ̸|= ϕ. Proof sketch. Let O = 〈R,F〉. Since O ̸|= ϕ there is a model M |= O with M ̸|= ϕ. The proof proceeds by defining a model I of rew∨(R) ∪ F such that I ̸|= ϕ. The extensions of ontology predicates in I is defined in a straightforward way by copying corresponding relationships on named elements fromM: - I |= Type(0, . . . , 0), Named(a), Top(a) for all a ∈ CO I |= A(a) for all A ∈ P1R \ {⊤, ⊥} with aM ∈ AM I |= R(a, b) for all R ∈ P2R with 〈aM, bM〉 ∈ RM - I |= Eq(a, b) if aM = bM Extensions for NamType and Type are defined in such a way that the true facts of these predicates correspond to all the (finitely many) types of named and unnamed elements that are realised in M, encoded in bits as explained before. It is not hard to check that the resulting interpretation I does indeed satisfy 〈rew∨(R), F〉. Lemma 4. For all fact sets F and all facts ϕ with a predicate in PR \ {⊤, ⊥, ≈}, if 〈rew∨(R), F〉 ̸|= ϕ then 〈R, F〉 ̸|= ϕ. Proof sketch. The proof inverts the argumentation used in Lemma 4. Since 〈rew∨(R),F〉 ̸|= ϕ, there is a model I |= rew∨(R) ∪ F with I ̸|= ϕ. To show 〈R,F〉 ̸|= ϕ, we define a model M |= R ∪ F with M ̸|= ϕ. This model is now constructed by combining the available types in a compatible way, which can be formalised as an iterative process. Initially, we define the named part of M, consisting of named individuals (factorised by equality) and their direct relations. In detail, let M = M0 with ∆M0 = {[a]≈ | a ∈ CR} where [a]≈ = {b | I |= Eq(a, b)}, and set aM0 = [a]≈ for all a ∈ CF. The interpretation of other c ∈ C \ CF is arbitrary. We set aM0 ∈ AM0 for A ∈ P1R if I |= A(a), and 〈aM0 , bM0 〉 ∈ RM0 for R ∈ P2R \ {≈} if I |= R(a, b). M0 then is expanded iteratively by adding elements for satisfying existential restrictions (marked ⃗Ei in Figure 2), which are taken from the available types. We avoid adding redundant successor elements, which is important to ensure the satisfaction of functionality axioms. This iterative construction leads to a monotonically increasing sequence of interpretationsM0,M1, . . . with union M = ⋃i≥0 Mi. We can show by induction that each Mi satisfies all of the Datalog∨ rules in R. The rules with existential quantifiers in R are satisfied by M because we apply the extension rule fairly to each domain element in ∆M. ## 4 ALCHIQ to Terminating Datalog∨∃ We will now specify a polynomial rewriting of ALCHIQ to Datalog∨∃ . Our main result improves upon Theorem 2 by avoiding the need for predicates of unbounded arity: Theorem 5. ALCHIQ is poly-time rewritable into terminating Datalog∨∃ rules of bounded size. For the remainder of this section, let R be an arbitrary, fixed ALCHIQ rule set. Moreover, let R∃ and R⩽ be the sets of all rules of type (∃) and (⩽) in R, respectively. Theorem 5 is established by the following rewriting. Definition 5. Let rew∨∃ (R) be the Datalog∨∃ rule set that contains the rules shown in Figure 5 and the rule set obtained from Ax(R\(R∃ ∪R⩽)) by replacing every predicate P with a fresh predicate P of the same arity. Note that Figure 5 uses predicates P and P, as well as further variants P ¬ and P¬, which indicate the absence of a true atom. The fresh predicates (i.e., predicates such as P) allow us to reserve regular ontology predicates for relations between named individuals, which we mark by Named. This relationship between the predicate names is expressed in the rules of (6). It is required since we often treat named individuals differently from individuals that were introduced to satisfy existential restrictions (see, e.g., rules of type (10)). Intuitively, the rules implement a proof procedure that is similar to tableau calculi in DLs, where we construct a finite representation of a model by applying rules for each type of axiom iteratively. For example, rules of type (9) introduce a successor element to satisfy an existential restriction. Essential tableau-like structures are captured by predicates Named and Unnamed, and by Succ (where Succ(x, y) means that y was created to satisfy an existential restriction on x). Facts SmClAi (x, y) mean that x and y agree on all classes A1, . . . , Ai for a fixed ordering A1, . . . , An ∈ P1R \ {⊤, ⊥}. Facts SmRlRi (x, y, z,w) are analogous for roles between class-equivalent pairs 〈x, y〉 and 〈z,w〉. The "equivalence" of elements y and w (SameTyp(y, w)) is inferred by (17). To ensure that the resulting structure is finite, however, we sometimes need to reuse anonymous elements. Tableau procedures accomplish this by a method known as blocking, and our approach is similar to pairwise anywhere blocking [Motik et al., 2009]. In contrast to tableau approaches, however, we cannot directly disallow the application of rule (9) (which would require non-monotonic negation). Instead, when we detect that two elements x and y are of the same type (17), we reuse all of the successors of either term that are introduced to satisfy rules of the form (9) to satisfy the same rules over the other element (18). Since we apply Datalog∨ rules with higher priority (Definition 3), rules (17) and (18) are preferred over rules of type (9). Therefore, we will not introduce a successor for x to satisfy an existential restriction if we already have introduced one such successor for y. This is essential for termination. Removing the rules (13)-(18) would still yield a correct rewriting from ALCHIQ into Datalog∨∃ , but the resulting rule set would not be terminating. Another peculiarity is the ternary predicate Copy, which is a weaker form of Eq that we use to handle functionality on unnamed individuals (10). If Copy(x, y, z) holds, then all unary relations of y and all binary relations between x and y are copied to z (rules (11) and (12)). Asserting Eq(y, z) would copy additional binary relations of y and other elements, which would not be sound in our case. Detailed proofs of soundness and correctness of Theorem 2 are found in our technical report [Carral and Kr¨otzsch, 2020]. ## 5 Horn-ALCHIQ to Datalog and Datalog∃ The rewritings of Sections 3 and 4 introduce disjunctions even if the input ontology is Horn. Alternative approaches, outlined next, can be used to prevent this. Ortiz et al. [2010] propose a polynomial translation from Horn-ALCHOIQ- the extension of Horn-ALCHIQ with R(x, y) ∧ R(x, z) ∧ Named(x) ∧ Named(y) ∧ Named(z) → Eq(y, z) | R(x, y) ∧ R(x, z) → y ≈ z ∈ R≤} ∪ {SameTyp(x, z) ∧ Succ(x, y) ∧ P(x, y) → Succ(z, y) ∧ P(z, y), Figure 5: Mapping the ALCHIQ Rule Set R into the Terminating Datalog∨∃ Rule Set rw4(R) (A1, . . . ,An and R1, . . . ,Rm are lists without repetitions containing all of the elements in P1R \ {⊤, ⊥} and P2R \ {≈}, respectively) nominals - to DatalogS - an extension of Datalog with set operators - and discuss how to transform the resulting DatalogS rule sets into Datalog in polynomial time. Applying this to Horn-ALCHIQ yields the following result. Theorem 6. Horn-ALCH(O)IQ is rewritable to Datalog in polynomial time. The rewriting shares some commonalities with the typebased method of Section 3, and in particular uses predicates of unbounded (though polynomial) arity for encoding sets. To get bounded-size rules, we can rewrite to Datalog∃ using a technique introduced by Carral et al. [2019a] for rewriting Horn-ALC to polynomial, bounded-size Datalog∃ . In their approach, an (existing) consequence-based reasoning procedure is expressed in a fixed set of DatalogS rules, which are then rewritten to terminating Datalog∃ [Carral et al., 2019a, Theorem 4]. A fundamental difference of this approach to our rewriting in Section 4 is that the whole ontology is rewritten into facts that are combined with a fixed Datalog∃ rule set. In a similar manner, one could adapt existing consequence-based reasoning procedures for Horn-ALCHIQ [Kazakov, 2009] to solve fact entailment, express the adapted procedure using a set of DatalogS rules, and then rewrite these rules into terminating Datalog∃ . Indeed, this strategy describes how compute a rewriting from Horn-ALCHIQ to Datalog∃ , and hence the following holds. Theorem 7. Horn-ALCHIQ is poly-time rewritable to terminating Datalog∃ rules of bounded size. Further details are found in our technical report [2020]. ## 6 FutureWork and Conclusions We show that ALCHIQ is poly rewritable to Datalog∨ and to bounded-size Datalog∨∃ for which the disjunctive chase terminates when prioritising non-generating rules ("Datalog∨- first"). As for future work, we aim to develop rewriting techniques for more expressive DL languages, such as ALCHOIQ, and decidable rule languages [Baget et al., 2011; K¨onig et al., 2015] to terminating Datalog∨∃ . Termination of our Datalog∨∃ rewritings relies on the use of the restricted chase with a Datalog∨-first rule application strategy. The set modelling technique used for Horn-ALCHIQ (Theorem 7) can be adapted to work for arbitrary strategies, but no such modification is known for our rewriting in Section 4. Bounded-size terminating rewritings may still be achieved, even when using the weaker Skolem chase [Marnette, 2009], by limiting the depth of terms in the chase using binary counters. However, this will result in a 2EXPTIME procedure, while our rewriting achieves NEXPTIME (cf. proof of Lemma 5). As for all known polynomial rewritings of non-Horn DLs with EXPTIME-complete reasoning problems, these are not worst-case optimal. The quest for optimal rule-based approaches in such cases remains open. ## Acknowledgements We thank Sebastian Rudolph for his helpful comments. This work was partly funded by Deutsche Forschungsgemeinschaft (DFG) grant 389792660 as part of TRR 248 and Emmy Noether grant KR 4381/1-1. ## References 1. [Ahmetaj et al., 2016] Shqiponja Ahmetaj, Magdalena Or- tiz, and Mantas Simkus. Polynomial Datalog rewritings for expressive Description Logics with closed predicates. In Subbarao Kambhampati, editor, Proc. 25th Int. Joint Conf. on Artif. Intell. (IJCAI 2016), pages 878-885. IJ- CAI/AAAI Press, 2016. 2. [Baget et al., 2011] Jean-Franc ¸ois Baget, Marie-Laure Mug- nier, Sebastian Rudolph, and Michaël Thomazo. Walk- ing the complexity lines for generalized guarded existen- tial rules. In Proc. 22nd Int. Joint Conf. on Artif. Intell. (IJCAI 2011), pages 712-717, 2011. 3. [Bellomarini et al., 2018] Luigi Bellomarini, Emanuel Sallinger, and Georg Gottlob. The Vadalog system: Datalog-based reasoning for knowledge graphs. PVLDB, 11(9):975-987, 2018. 4. [Bienvenu et al., 2014] Meghyn Bienvenu, Balder ten Cate, Carsten Lutz, and Frank Wolter. Ontology-based data ac- cess: A study through disjunctive Datalog, CSP, and MM- SNP. ACM Transactions of Database Systems, 39(4):33:1- 33:44, 2014. 5. [Carral and Krötzsch, 2020] David Carral and Markus Krötzsch. Rewriting the description logic ALCHIQ to disjunctive existential rules: Technical report. Available at https://iccl.inf.tu-dresden.de/web/Inproceedings3244/en, 2020. 6. [Carral et al., 2018] David Carral, Irina Dragoste, and Markus Krötzsch. The combined approach to query an- swering in Horn-ALCHOIQ. In Michael Thielscher, Francesca Toni, and Frank Wolter, editors, Proc. 16th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 2018), pages 339-348. AAAI Press, 2018. 7. [Carral et al., 2019a] David Carral, Irina Dragoste, Markus Krötzsch, and Christian Lewe. Chasing sets: How to use existential rules for expressive reasoning. In Sarit Kraus, editor, Proc. 28th Int. Joint Conf. on Artif. Intell. (IJCAI 2019), pages 1624-1631. ijcai.org, 2019. 8. [Carral et al., 2019b] David Carral, Larry González, and Patrick Koopmann. From Horn-SRIQ to Datalog: A data-independent transformation that preserves assertion entailment. In Proc. 33rd AAAI Conf. on Artificial Intelli- gence (AAAI 2019), pages 2736-2743. AAAI Press, 2019. 9. [Eiter et al., 2012] Thomas Eiter, Magdalena Ortiz, Man- tas Simkus, Trung-Kien Tran, and Guohui Xiao. Query rewriting for Horn-SHIQ plus rules. In Jörg Hoffmann and Bart Selman, editors, Proc. 26th AAAI Conf. on Artifi- cial Intelligence (AAAI 2012). AAAI Press, 2012. 10. [Horrocks et al., 2000] Ian Horrocks, Ulrike Sattler, and Stephan Tobies. Practical reasoning for very expressive Description Logics. Logic J. of the IGPL, 8(3):239-263, 2000. 11. [Hustadt et al., 2007] Ullrich Hustadt, Boris Motik, and Ul- rike Sattler. Reasoning in Description Logics by a re- duction to disjunctive Datalog. J. Automated Reasoning, 39(3):351-384, 2007. 12. [Kazakov et al., 2013] Yevgeny Kazakov, Markus Krötzsch, and František Simančík. The incredible ELK: From poly- nomial procedures to efficient reasoning with EL ontolo- gies. J. Automated Reasoning, 53:1-61, 2013. 13. [Kazakov, 2009] Yevgeny Kazakov. Consequence-driven reasoning for Horn-SHIQ ontologies. In Proc. 21st Int. Joint Conf. on Artif. Intell. (IJCAI 2009), pages 2040- 2045, 2009. 14. [König et al., 2015] Mélanie König, Michel Leclère, Marie- Laure Mugnier, and Michaël Thomazo. Sound, complete and minimal UCQ-rewriting for existential rules. Semantic Web, 6(5):451-475, 2015. 15. [Krötzsch, 2011] Markus Krötzsch. Efficient rule-based in- ferencing for OWL EL. In Toby Walsh, editor, Proc. 22nd Int. Joint Conf. on Artif. Intell. (IJCAI 2011), pages 2668- 2673. IJCAI/AAAI, 2011. 16. [Lifschitz, 2019] Vladimir Lifschitz. Answer Set Program- ming. Springer, 2019. 17. [Marnette, 2009] Bruno Marnette. Generalized schema- mappings: from termination to tractability. In Jan Paredaens and Jianwen Su, editors, Proc. 28th ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS 2009), pages 13-22. ACM, 2009. 18. [Motik et al., 2009] Boris Motik, Rob Shearer, and Ian Hor- rocks. Hypertableau reasoning for description logics. J. Artif. Intell. Res., 36:165-228, 2009. 19. [Motik et al., 2014] Boris Motik, Yavor Nenov, Robert Piro, Ian Horrocks, and Dan Olteanu. Parallel materialisation of Datalog programs in centralised, main-memory RDF sys- tems. In Proc. 28th AAAI Conf. on Artificial Intelligence (AAAI 2014), pages 129-137, 2014. 20. [Ortiz et al., 2010] Magdalena Ortiz, Sebastian Rudolph, and Mantas Simkus. Worst-case optimal reasoning for the Horn-DL fragments of OWL 1 and 2. In Fangzhen Lin, Ulrike Sattler, and Miroslaw Truszczynski, editors, Proc. 12th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 2010). AAAI Press, 2010. 21. [Rudolph et al., 2012] Sebastian Rudolph, Markus Krötzsch, and Pascal Hitzler. Type-elimination-based reasoning for the Description Logic SHIQb s using decision diagrams and disjunctive Datalog. Logical Methods in Computer Science, 8(1), 2012. 22. [Simancik, 2012] Frantisek Simancik. Elimination of com- plex RIAs without automata. In Yevgeny Kazakov, Domenico Lembo, and Frank Wolter, editors, Proc. 25th Int. Workshop on Description Logics (DL 2012), volume 846 of CEUR Workshop Proceedings. CEUR-WS.org, 2012. 23. [Urbani et al., 2018] Jacopo Urbani, Markus Krötzsch, Ceriel J. H. Jacobs, Irina Dragoste, and David Carral. Efficient model construction for Horn logic with VLog -system description. In Proc. 9th Int. Joint Conf. on Automated Reasoning (IJCAR 2018), Held as Part of the Federated Logic Conference (FloC 2018), pages 680-688, 2018.