Rewriting the Description Logic ALCHIQ to Disjunctive Existential Rules

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

†: 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.

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∨);
6. 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.

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.