Horn Rewritability vs PTime Query Evaluation for Description Logic TBoxes André Hernich1 , Carsten Lutz2 , Fabio Papacchini1 , and Frank Wolter1 1 University of Liverpool, UK, {firstname.surname}@liverpool.ac.uk 2 University of Bremen, Germany, clu@uni-bremen.de Abstract. We study the following question: if T is a TBox that is formulated in an expressive DL L and all CQs can be evaluated in PTime w.r.t. T , can T be replaced by a TBox T 0 that is formulated in the Horn-fragment of L and such that for all CQs and ABoxes, the answers w.r.t. T and T 0 coincide? Our main results are that this is indeed the case when L is the set of ALCHI or ALCIF TBoxes of quantifier depth 1 (which covers the majority of such TBoxes), but not for ALCHIF and ALCQ TBoxes of depth 1. 1 Introduction In ontology-mediated querying, TBoxes are used to enrich incomplete data with domain knowledge, enabling more complete answers to queries [30, 5, 22]. Since query evaluation is coNP-hard in the presence of TBoxes formulated in expressive description logics (DLs) such as ALC and SHIQ [31, 23, 14], the identification of computationally more well-behaved setups has been an important goal of research [1, 9, 8, 28]. In particular, this has led to the introduction of Horn-DLs, syntactically defined fragments of expressive DLs that fall within the Horn- fragment of first-order logic [16, 29]. Widely known examples include the fragment Horn-SHIQ of SHIQ and the corresponding fragment Horn-ALC of ALC [16, 4]. In contrast to the expressive DLs in which they are included, these Horn-DLs admit the construction of universal models giving exactly the same answers to queries as the class of all models of a knowledge base. The existence of universal models can then be used to show that query evaluation is in PTime in data complexity, and to design practical query answering algorithms [12, 29, 21]. Thus, any TBox formulated in an expressive DL that falls within the corresponding Horn-DL is computationally well-behaved. In this paper, we ask the converse question, concentrating on conjunctive queries (CQs): is it the case that every TBox T formulated in an expressive DL and for which CQ-evaluation is in PTime is rewritable into a TBox T 0 formulated in the corresponding Horn-DL? If one requires T to be logically equivalent to T 0 , then the answer is “no” even for the basic expressive DL ALC. But logical equivalence is an unnecessarily strong requirement in the context of ontology- mediated querying where it typically suffices to demand CQ-inseparability, that is, T and T 0 should give exactly the same answers to any CQ on any ABox; see for example [26, 6, 7] for more on CQ-inseparability. For an expressive DL L, we are thus interested in the following property: we say that rewritability into CQ- inseparable Horn-TBoxes captures PTime query evaluation if for every L TBox T such that CQ-evaluation w.r.t T is in PTime there exists a Horn-L TBox T 0 such that T and T 0 are CQ-inseparable. Note that when L satisfies this property, then one can replace any L TBox T that enjoys PTime CQ-evaluation by its rewriting T 0 and take advantage of the algorithms available for CQ-evaluation w.r.t. Horn-L TBoxes without affecting the answers to CQs. The main result of this paper states that rewritability into CQ-inseparable Horn-TBoxes captures PTime query evaluation when L is the class of ALCHIF TBoxes of depth one in which no role is included in a functional role, where the depth of a TBox is the nesting depth of quantifiers in its concepts. Despite the restriction to depth one, this result is rather general. We have analyzed 411 ontologies from the BioPortal repository. After removing all constructors that do not fall within ALCHIF, 385 ontologies had depth 1 (sometimes modulo an easy equivalent rewriting). Moreover, the pre-processing used in most DL reasoners transforms an input TBox into a TBox of depth one by structural transformation. In our proof we show how to construct from a TBox T formulated in L a canonical Horn-TBox Thorn such that Thorn is a CQ-inseparable rewriting of T if and only if CQ-evaluation w.r.t. T is in PTime. Informally, Thorn is constructed by first normalising T and then composing concept inclusions from the concepts in the normalised TBox. The correctness proof makes use of the fact that for ALCHIF TBoxes of depth one, CQ-evaluation is in PTime iff the TBox admits universal models [15, 27]. We then show that this result is optimal in several ways. For example, the restriction regarding the interaction of role inclusions and functional roles cannot be dropped since for unrestricted ALCHIF TBoxes of depth one, rewritability into CQ-inseparable Horn-TBoxes does not capture PTime query evaluation. We also show such a negative result for ALCQ TBoxes of depth one. Both results rely on the unique name assumption, which we generally make in this paper. Regarding TBoxes of depth larger than one, we remark that it is known that for ALC TBoxes of depth three rewritability into CQ-inseparable Horn-TBoxes does not capture PTime query evaluation [27]; the status of ALC TBoxes of depth two is open. Related Work. Rewritability from one language into another has been studied extensively in description logic. A large body of work investigates (the existence of) rewritings of ontology-mediated queries (OMQs) into an FO query or Datalog query that gives the same answers over all ABoxes [3, 4, 13]. The main difference to the work presented in this paper is that both the TBox and the CQ are given as input whereas in this paper we quantify over all CQs. In [18, 17, 10], the authors consider Horn-DL and EL rewritability of OMQs with atomic queries. Also closely related is work on the rewritability of TBoxes formulated in an expressive DL into a TBox formulated in a weaker DL that is either equivalent to or a conservative extension of the original TBox [25, 20]. 2 Preliminaries We use the notation from [2]. Let NC and NR be countably infinite sets of concept and role names, respectively. A role is a role name or the inverse r− of a role name r. For standard DLs L between ALC and ALCHIQ we define L concept inclusions (CIs) and L TBoxes in the usual way. The functionality assertions in ALCF and its extensions take the form func(r), where r is a role name (a role if the DL admits inverse roles). Role inclusions (RIs) in ALCH and its extensions take the form r v s, where r and s are role names (roles if the DL admits inverse roles). The only non-standard DL we consider is ALCF ` which is located between ALCF and ALCQ and in which one can use in addition to the constructors of ALC local functionality restrictions of the form (≤ 1r). In certain normal forms we also use ELI concepts which are constructed using >, u, and ∃r.C, r a role. An ABox A is a non-empty finite set of assertions of the form A(a) and r(a, b) with A ∈ NC , r ∈ NR , and a, b individual names. Interpretations I and the extension C I of a concept C are defined as usual. An interpretation I satisfies a CI C v D if C I ⊆ DI , an RI r v s if rI ⊆ sI , an assertion A(a) if a ∈ AI , an assertion r(a, b) if (a, b) ∈ rI , and a functionality assertion func(r) if rI is a partial function. Note that we make the standard name assumption, that is, individual names are interpreted as themselves. This implies the unique name assumption. An interpretation I is a model of a TBox T if it satisfies all inclusions and assertions in T and I is a model of an ABox A if it satisfies all assertions in A. We call an ABox A satisfiable w.r.t. a TBox T if A and T have a common model. The depth of an ALCI concept is the maximal number of nestings of the operators ∃r.C and ∀r.C in it; thus ∃r.A has depth 1 and ∃r.∀r.A has depth 2. For DLs with number restrictions, nestings of number restrictions also contribute to the depth. The depth of a TBox is the maximal depth of the concepts that occur in it. A Horn-ALCI CI takes the form L v R, where L and R are built according to the following syntax rules: R, R0 ::= > | ⊥ | A | ¬A | R u R0 | ¬L t R | ∃r.R | ∀r.R L, L0 ::= > | ⊥ | A | L u L0 | L t L0 | ∃r.L A Horn-ALCHIF TBox is a finite set of Horn-ALCI CIs, RIs, and functionality assertions. Note that there are several alternative ways to define Horn-DLs [16, 24, 12, 19], our definition is from [27]. The results in this paper remain valid under the alternative definitions. For a TBox T , ABox A and conjunctive query (CQ) q(x) we say that a tuple a of individuals in A of the same length as x is a certain answer to q(x) over A w.r.t. T , in symbols T , A |= q(a), if I |= q(a) holds for all models I of T and A. The query evaluation problem for T and CQ q is the problem to decide for an ABox A and a tuple a of individuals from A, whether T , A |= q(a). The CQ-evaluation problem for T is in PTime if the query evaluation problem for T and q is in PTime for every CQ q. The depth of TBoxes will play an important role in this paper. For deciding satisfiability and subsumption, TBoxes are often normalized to depth 1 in a pre-processing step. Since we are universally quantifying over all queries when defining the complexity of a TBox, such normalizations do not work in the sense that they can change the complexity of the TBox, see [27, 15]. To show that a TBox cannot be rewritten into a CQ-inseparable Horn- TBox, we shall sometimes use products of interpretations; we only need the product of two interpretations, see [11, 25] for the general case. Let I1 and I2 be interpretations. Then the product I1 × I2 of I1 and I2 is defined by setting ∆I1 ×I2 = ∆I1 × ∆I2 AI1 ×I2 = {(d1 , d2 ) | d1 ∈ AI1 , d2 ∈ AI2 } rI1 ×I2 = {((d1 , d2 ), (e1 , e2 )) | (d1 , e1 ) ∈ rI1 , (d2 , e2 ) ∈ rI2 } Lemma 1. Every Horn-ALCHIQ TBox T is preserved under products: if I1 and I2 are models of T , then I1 × I2 is a model of T . 3 Horn Rewritability In this paper, we aim to understand whether and when a TBox formulated in an expressive DL can be replaced with a TBox formulated in the corresponding Horn-DL (e.g. an ALCHIF TBox by a Horn-ALCHIF TBox) without changing the answers to CQs. Following [26, 6, 7], TBoxes T1 and T2 are CQ-inseparable if for all CQs q, all ABoxes A, and all tuples a of individual names in A we have T1 , A |= q(a) iff T2 , A |= q(a). We say that rewritability into CQ-inseparable Horn-TBoxes captures PTime query evaluation for a DL L if for every L TBox T such that CQ evaluation w.r.t. T is in PTime, there is a Horn-L TBox T 0 such that T and T 0 are CQ-inseparable. The following example shows that rewritability into a CQ-inseparable Horn-TBox is a weaker notion than rewritability into a Horn-TBox that is logically equivalent. Example 1. Consider the Horn-ALC TBox T = {∃r.(A u ¬B u ¬E) v ∃r.(¬A u ¬B u ¬E)}. It is easy to see that for any CQ q(x), ABox A, and tuple a of individuals from A, we have T , A |= q(a) iff ∅, A |= q(a). Thus, CQ evaluation w.r.t. T is in PTime (actually in AC0 ). T is, however, not equivalent to any TBox preserved under products: consider interpretations I1 and I2 with ∆Ii = {0, 1}, rIi = {(0, 1)}, and AIi = {1} for i = 1, 2, but B I1 = {1}, E I1 = ∅, B I2 = ∅, and E I2 = {1}. Then Ii is a model of T for i = 1, 2, but I1 × I2 is not. Consequently, T is not equivalent to any Horn-TBox. We shall make use of several characterizations of CQ evaluation w.r.t. a TBox being in PTime that have been obtained in [15]. A TBox T is materializable if for any ABox A that is satisfiable w.r.t T there exists a model I of T and A such that for all CQs q(x) and all tuples a of individuals in A, T , A |= q(a) iff I |= q(a). T has the disjunction property for CQs if forWany ABox A, CQs q1 , . . . , qn and tuples a1 , . . . , an of individuals in A, T , A |= 1≤i≤n qi (ai ) implies that there is a j with T , A |= qj (aj ). An ontology-mediated query (OMQ) is a pair (T , q) with T a TBox and q a CQ. A Datalog6= program is a Datalog program that admits inequalities in the body of its rules. We say that (T , q) is Datalog6= rewritable if there is a Datalog6= -program Π such that for any ABox A and tuple a of individuals in A, T , A |= q(a) iff A |= Π(a). Theorem 1. [15] The following conditions are equivalent for all ALCHIF TBoxes T of depth 2 and all ALCHIQ TBoxes T of depth 1: 1. CQ evaluation w.r.t. T is in PTime; 2. T is materializable; 3. T has the disjunction property for CQs; 4. For every CQ q, the OMQ (T , q) is Datalog6= rewritable. Otherwise, CQ evaluation w.r.t. T is coNP-hard. Theorem 1 is optimal in many ways. For example, the following is shown in [15]: – the equivalence of Datalog6= -rewritability and PTime CQ evaluation does not hold for ALCF ` TBoxes of depth 2 and ALC TBoxes of depth 3. – there are ALCIQ TBoxes T of depth 2 such that CQ-evaluation w.r.t. T is neither in PTime nor coNP-hard. 4 Negative Results It follows from results in [15] that there are DLs in which rewritability into CQ-inseparable Horn-TBoxes does not capture PTime query evaluation. In fact, we have seen above that there are ALCF ` TBoxes of depth 2 and ALC TBoxes of depth 3 such that CQ evaluation w.r.t. T is in PTime but not every OMQ (T , q) is Datalog6= -rewritable. On the other hand, it is well known that every OMQ (T , q) with T a Horn-ALCHIQ TBox is Datalog6= -rewritable [15]. We thus obtain the following. Theorem 2. For ALCF ` TBoxes of depth 2 and ALC TBoxes of depth 3, rewritability into CQ-inseparable Horn-TBoxes does not capture PTime query evaluation. We next prove a negative result for ALCQ TBoxes of depth 1. Note that by Theorem 1, any ALCQ TBox T of depth 1 such that CQ evaluation w.r.t. T is in PTime is rewritable into Datalog6= . We thus need a different argument as in the proof of Theorem 2. This argument is based on products and actually establishes a stronger statement than aimed at, implying for example that not even rewritability into CQ-inseparable Horn-FO TBoxes captures PTime query evaluation. Theorem 3. For ALCQ TBoxes of depth 1, rewritability into CQ-inseparable Horn-TBoxes does not capture PTime query evaluation. Proof. Consider the TBox T = {(≥ 3r) v A}. It is easy to show that T is materializable. Thus, by Theorem 1, CQ evaluation w.r.t. T is in PTime. Assume that T is CQ-inseparable from a TBox T 0 . We show that T 0 is not preserved under products and thus not a Horn-ALCQ TBox. We have T 0 |= (≥ 3r) v A since, for A = {r(a, b1 ), r(a, b2 ), r(a, b3 )}, we have T , A |= A(a) and thus T 0 , A |= A(a). We also have T 0 6|= (≥ 2r) v A since, for A = {r(a, b1 ), r(a, b2 )}, we have T , A 6|= A(a) and thus T 0 , A 6|= A(a). Take a model I of T 0 with d ∈ (≥ 2r)I but d 6∈ AI . Then (d, d) ∈ (≥ 3r)I×I and (d, d) 6∈ AI×I . Thus I × I is not a model of T 0 . t u We now prove a similar negative result for ALCHIF TBoxes of depth 1. Theorem 4. For ALCHIF TBoxes of depth 1, rewritability into CQ-inseparable Horn-TBoxes does not capture PTime query evaluation. Proof. Let T be the ALCHIF TBox that states that role names s1 and s2 are functional and contains the RIs r v s1 and r v s2 and the CIs ∃s1 .(B1 u B2 ) v ∃r.> ∃s1 .> u ∃s2 .> v ∀s1 .B1 u ∀s2 .B2 ∃s1 .> u ∃s2 .> v B t ∃r.> We first show that T is materializable and so, by Theorem 1, CQ evaluation w.r.t. T is in PTime. Let A be an ABox. Due to the disjunction in the final CI, we have to distinguish two kinds of individuals a when constructing a materialization of A. Informally: – if a has distinct s1 - and s2 -successors, then a having an r-successor contradicts the role inclusions and s1 , s2 being functional and thus we want to make B true at a; – if a has a common s1 - and s2 -successor, then ∃r.> is implied at a. Formally, we construct the materialization of A as follows. Whenever a has both an s1 -successor and an s2 -successor, then add Bi to all its si -successors, i ∈ {1, 2}. Next, for any a that has an s1 -successor b in B1 u B2 , add r(a, b) and s2 (a, b) to the ABox. Denote the resulting ABox by A0 . If s1 or s2 are not functional in A0 , then A is not satisfiable w.r.t. T . Otherwise, a materialization is obtained by adding B(a) whenever a has distinct s1 - and s2 -successors. Assume that T 0 is CQ-inseparable from the TBox T . We show that T 0 is not preserved under products, thus not a Horn-ALCHIF TBox. Let A1 = {s1 (a, b1 ), s2 (a, b2 )}, A2 = {s1 (a, b), s2 (a, b)}. Then T , A1 |= B(a) and T , A2 |= ∃r.>(a), but T , A1 6|= ∃r.>(a) and T , A2 6|= B(a). Because of CQ-inseparability, the same hold when T is replaced with T 0 . Take a model I1 of T 0 and A1 with a 6∈ (∃r.>)I1 and a model I2 of T 0 and A2 with a 6∈ B I2 . Then I1 × I2 is a model of A1 (for a identified with (a, a), b1 with (b1 , b) and b2 with (b2 , b)). However, we do not have a ∈ B I1 ×I2 and since T 0 , A1 |= B(a) it follows that I1 × I2 is not a model of T 0 . t u 5 Horn Rewritability in ALCHIF We introduce a mild restriction on ALCHIF TBoxes regarding the interaction between RIs and functionality assertions and show that this restriction is sufficient to overcome the negative result stated in Theorem 4. Notably, the restricted form of ALCHIF TBoxes encompasses both (unrestricted) ALCHI TBoxes and ALCIF TBoxes. An ALCHIF vf TBox is an ALCHIF TBox T such that whenever r v s ∈ T , then neither s nor s− are functional in T . The aim of this section is to prove the following result. Theorem 5. For ALCHIF vf TBoxes of depth 1, rewritability into CQ-in- separable Horn-TBoxes captures PTime query evaluation. We start by introducing a normal form for ALCHIF TBoxes of depth 1. A literal is a concept name or a negation thereof. A CI C v D is in normal form if 1. C is an ELI-concept of depth 1; 2. D is a disjunction of – concept names; – concepts ∃r.E with E a conjunction of literals; – concepts ∀r.E with E a disjunction of literals that contains at least one positive literal. We set C = > if C is the empty conjunction and D = ⊥ if D is the empty disjunction. Given a set F of functionality assertions func(r), we can normalise CIs further by demanding that in C v D for each r such that func(r) ∈ F: – any ∃r.D0 in D contains only positive literals; – if there exists an ∃r.C 0 in C, then this is the only occurrence of r in C v D; – if there exists a ∀r.D0 in D, then this is the only occurrence of r in C v D. We then call C v D in normal form relative to F. An ALCHIF TBox T is in normal form if all its CIs are in normal form relative to the functionality assertions in T . The following result is shown in the full version of this paper available at http://cgi.csc.liv.ac.uk/ frank/publ/publ.html. Lemma 2. Every ALCHIF vf TBox T of depth 1 can be converted into a logically equivalent ALCHIF vf TBox T 0 in normal form. T 0 is of size at most single exponential in |T |. Example 2. The TBox T from Example 1 can be transformed into the TBox T 0 = {∃r.A v ∃r.(¬A u ¬B u ¬E) t ∀r.(A → B t E)}, which is in normal form. If r is functional, one obtains {> v ∀r.(A → B t E)}. We now identify a basic yet crucial property of ALCHIF vf TBoxes T . For any ELI concept C of depth 1 that contains at most one conjunct of the form ∃r.C 0 per functional role r one can define in a straightforward way a tree-shaped ABox AC of depth 1 with root ρC that corresponds to C. For example, when C = ∃r.> u ∃s.(A u B) then AC = {r(ρC , b1 ), s(ρC , b2 ), A(b2 ), B(b2 )}. Then one can prove the following: Lemma 3. For every ALCI-concept D, T |= C v D iff T , AC |= D(ρC ). Note that Lemma 3 fails for unrestricted ALCHIF TBoxes. Consider for example the TBox T and ABox A1 from the proof of Theorem 4 and let CA1 be A1 viewed as an EL-concept. Then T 6|= CA1 v B, but T , A1 |= B(a). We next introduce some preliminaries needed for constructing the desired Horn-ALCHIF vf TBoxes that are CQ-inseparable from a given ALCHIF vf TBox of depth 1. For any conjunction or disjunction of literals E, we use pos(E) to denote the set of concept names A in E and neg(E) to denote the set of concept names A such that ¬A in E. If ∀r.E is a universal restriction with E a disjunction of literals that contains at least one positive literal, then a Horn specialization of ∀r.E is a concept ∀r.E 0 where E 0 is obtained from E by dropping all but one positive literal. Note that any Horn specialization can be written in the form ∀r.(A1 u · · · u An → A). For an ALCHIF vf TBox T in normal form, we use LT to denote the set of – concept names or existential restrictions that occur on top-level on the left-hand side of some CI in T ; – concepts ∃r.neg(E) such that there is a CI in T whose right-hand side contains a disjunct ∀r.E. A set S ⊆ LT is a trigger for a CI C v D ∈ T if S contains all top-level conjuncts of C and all ∃r.neg(E) with ∀r.E a disjunct of D. For a trigger S, we denote by CS the conjunction of all concept names in S, all existential restrictions ∃r.C 0 ∈ S with r not functional, and all ∃r.(C1 u· · ·uCn ) where r is functional and C1 , . . . , Cn is the set of all concepts such that ∃r.Ci ∈ S. For each CI C v D ∈ T and trigger S for it, we define a set Horn(C v D, S) of Horn-ALCHIF vf CIs. As a special case, Horn(C v D, S) is {CS v ⊥} if T |= CS v ⊥. Otherwise, Horn(C v D, S) consists of the following CIs whenever they are a consequence of T: – CS v A with A a concept name in D; – CS v R with R = ∀r.(A1 u· · ·uAn → A) a Horn restriction of some universal restriction in D; – CS v ∃r.pos(E) with ∃r.E an existential restriction in D such that T 6|= CS v ¬∃r.E. Define a Horn-ALCHIF TBox Thorn as the union of all functionality assertions and RIs in T and [ Horn(C v D, S) CvD∈T , S trigger for CvD Observe that, by construction, T |= Thorn . Example 3. For the TBox T 0 from Example 2 we have LT 0 = {∃r.A, ∃r.>} and thus {∃r.A} is the only trigger for ∃r.A v ∃r.(¬Au¬B u¬E)t∀r.(A → B tE) up 0 to logical equivalence. Thus, Thorn = {∃r.A v ∃r.>} which is logically equivalent to the empty TBox. Now, Theorem 5 is a consequence of Theorem 1 and the “(1.) ⇒ (3.)” part of the following result. Theorem 6. Let T be a ALCHIF vf TBox in normal form. Then the following conditions are equivalent: 1. T has the disjunction property for CQs; 2. for every C v D ∈ T and trigger S for C v D, Horn(C v D, S) 6= ∅. 3. T and Thorn are CQ-inseparable. Proof. (3) ⇒ (1.) follows from Theorem 1 since CQ-evaluation is in PTime if T and Thorn are CQ-inseparable. (1.) ⇒ (2.). Assume T has the disjunction property for CQs and assume that there are C v D ∈ T and a trigger S for C v D such that Horn(C v D, S) = ∅. Let A1 , . . . , Ak , ∃r1 .E1 , . . . , ∃rn .En , and ∀s1 .F1 , . . . , ∀sm .Fm be the disjuncts of D such that T 6|= CS v ¬∃ri .Ei for 1 ≤ i ≤ n. Let ACS be CS viewed as an ABox with root a0 , and let a1 , . . . , am be the individuals in ACS introduced for the existential restrictions ∃si .neg(Fi ) in CS . By Lemma 3, we have: _ _ _ _ T , ACS |= Ai (a0 ) ∨ ∃ri .pos(Ei )(a0 ) ∨ A(ai ). i=1..k i=1..n i=1..m A∈pos(Fi ) By the disjunction property for CQs of T and Lemma 3 at least one of the disjuncts F (a) is entailed. We obtain: – if F (a) = Ai (a0 ) then T |= CS v Ai ; – if F (a) = A(ai ) for some A ∈ pos(Fi ), then T |= CS v ∀si .(neg(Fi ) → A); – if F (a) = ∃ri .pos(Ei )(a0 ), then T |= CS v ∃ri .pos(Ei ). In each case, we obtain an α ∈ Horn(C v D, S) and thus derive a contradiction. (2.) ⇒ (3.). Assume (2.) holds. It suffices to show that for every ABox A the following holds: if A is satisfiable relative to Thorn , then there exists a materialization U of A and Thorn that is a model of T . U is constructed using the following set RT of chase rules: 1. if (d, e) ∈ rI and r v s ∈ T , then add (d, e) to sI ; 2. if d ∈ C I and C v A ∈ Thorn , then add d to AI ; 3. if d ∈ C I and C v R ∈ Thorn for R = ∀r.(A1 u · · · u An → A), then add e to AI whenever (d, e) ∈ rI and e ∈ (A1 u · · · u An )I . 4. if d ∈ C I and C v ∃r.pos(E) ∈ Thorn then (i) if r is functional and there exists e with (d, e) ∈ rI add e to F I for all concept names F in pos(E) and (ii) otherwise take a fresh element e, add (d, e) to rI and add e to F I for all concept names in pos(E). This rule is applied at most once for any pair (d, ∃r.E) with ∃r.E on the right hand side of a CI in Thorn . The element e required by this rule is called the witness for ∃r.E at d. The interpretation U is the limit of the sequence I0 , I1 , . . . obtained from the interpretation I0 corresponding to the ABox A by applying the rules in RT in a fair way. It is standard to prove that U is a materialization of A and Thorn if A is satisfiable w.r.t. Thorn (here one uses that T does not contain any functional roles s with T |= r v s for an r 6= s). Our aim now is to prove that U is a model of T . We proceed in two steps. Let d ∈ ∆U and assume that the chase introduces e as a witness for ∃r.E at d. We say that this witness has been invalidated if e ∈ / E U . Observe that if r is a functional role then for any C v ∃r.pos(E) ∈ Thorn we have E = pos(E). Thus for functional roles r no witnesses for ∃r.E can be invalidated. For an interpretation I and d ∈ ∆I we denote by eltpTU (d) the set of all F ∈ LT such that d ∈ F I . Claim 1. If the witness for ∃r.E at d was invalidated, then Thorn |= CS v ¬∃r.E for S = eltpTU (d). For the proof of Claim 1, denote by ACS the ABox with root ρS corresponding ∃r.pos(E) to CS . Denote by ACS the extension of ACS with a fresh individual e and fresh assertions r(ρF , e) and A(e) for A ∈ pos(E). We now apply the chase ∃r.pos(E) procedure for Thorn to ACS rather that A and obtain a materialization U 0 ∃r.pos(E) of ACS and Thorn . Using the fact that the CIs of Thorn have depth 1 and the condition that the witness for ∃r.E at d was invalidated in the chase applied to ∃r.pos(E) 0 A one can readily show that it is invalidated in ACS as well. Thus e 6∈ E U and it follows with Lemma 3 that Thorn |= CS v ¬∃r.E. Claim 2. U is a model of T . Let C v D ∈ T and d ∈ C U . We show that d ∈ DU . For a proof by contradiction assume that this is not the case. Then the set S = eltpTU (d) is a trigger for C v D. By (2.) there exists α ∈ Horn(C v D, S). We obtain that at least one of the following holds: 1. there is a concept name A in D such that T |= CS v A. Then CS v A ∈ Thorn and so d ∈ AU . Thus d ∈ DU and we have derived a contradiction. 2. there is a universal restriction R = ∀r.(A1 u · · · u An → A) that is a Horn restriction of some universal restriction in D such that T |= CS v R. Then CS v R ∈ Thorn and so d ∈ RU . Thus d ∈ DU and we have derived a contradiction. 3. there is an ∃r.E in D such that T |= CS v ∃r.pos(E) and T 6|= CS v ¬∃r.E. Then there exists e ∈ ∆U with (d, e) ∈ rU such that e ∈ pos(E)U . By Claim 1, the witness e for ∃r.E at d was not invalidated. Thus d ∈ (∃r.E)U . Hence d ∈ DU and we have derived a contradiction. This finishes the proof of Theorem 6. t u The following example shows that Thorn can be of exponential size in |T | even if redundant CIs are removed. Example 4. Let T n contain Bi v ∀s.Ai ∃r.> v ∃s.> B̂i v ∀s.Ai ∃r.> v A t t ∃s.¬Ai 1≤i≤n n where 1 ≤ i ≤ n. The TBox Thorn is obtained from Tn by replacing the final CI by the set of CIs ∃r.> u u Ci v A 1≤i≤n n where Ci ∈ {Bi , B̂i }. Then Thorn and T n are CQ-inseparable and Thorn n is of n exponential size in |T |. n Clearly, the TBoxes Thorn can be equivalently expressed by Horn-TBoxes of n polynomial size in |T | by introducing disjunctions on the left-had side of CIs. In fact, it remains open whether for every ALCHIF vf TBoxes in normal form for which CQ-evaluation is in PTime there exists a CQ-inseparable Horn- ALCHIF vf TBox of polynomial size. 6 Conclusion We have shown that rewritability into CQ-inseparable Horn-TBoxes captures PTime query evaluation for ALCHIF TBoxes of depth 1 in which no role is included in a functional role. Interestingly, this result also implies that CQ- inseparable rewritability into Horn-TBoxes is decidable and ExpTime-complete for such ALCHIF TBoxes since it is shown in [15] that deciding whether CQ- evaluation is in PTime for ALCHIF TBoxes of depth 1 is ExpTime-complete. We have also shown that for arbitrary ALCHIF and ALCQ TBoxes of depth 1, rewritability into CQ-inseparable Horn-TBoxes does not capture PTime query evaluation. These negative results depend on the unique name assumption we make in this paper. In fact, it is not difficult to see that CQ-evaluation is coNP- hard for the TBoxes used in the proofs of Theorems 3 and 4 and so they cannot serve as counterexamples anymore. We conjecture that without the unique name assumption one can generalize our positive result and show that rewritability into CQ-inseparable Horn-TBoxes captures PTime query evaluation for arbitrary ALCHIQ TBoxes of depth 1. Observe that for TBoxes not using functional roles or qualified number restrictions CQ-evaluation does not depend on whether one makes the unique name assumption or not. Thus, the negative result that for ALC TBoxes of depth 3 CQ-inseparable Horn-TBoxes do not capture PTime query evaluation does not depend on the unique name assumption. It remains an interesting open question whether rewritability into CQ-inseparable Horn-TBoxes captures PTime query evaluation for ALC or ALCI TBoxes of depth 2. Acknowledgements André Hernich, Fabio Papacchini, and Frank Wolter were supported by EPSRC UK grant EP/M012646/1. Carsten Lutz acknowledges support by the DFG-funded Collaborative Research Center EASE. References 1. Artale, A., Calvanese, D., Kontchakov, R., Zakharyaschev, M.: The DL-Lite family and relations. J. of Artifical Intelligence Research 36, 1–69 (2009) 2. Baader, F., Horrocks, I., Lutz, C., Sattler, U.: An Introduction to Description Logics. Cambride University Press (2017) 3. Bienvenu, M., ten Cate, B., Lutz, C., Wolter, F.: Ontology-based data access: A study through disjunctive datalog, csp, and MMSNP. ACM Trans. Database Syst. 39(4), 33:1–33:44 (2014) 4. Bienvenu, M., Hansen, P., Lutz, C., Wolter, F.: First order-rewritability and con- tainment of conjunctive queries in horn description logics. In: IJCAI. pp. 965–971 (2016) 5. Bienvenu, M., Ortiz, M.: Ontology-mediated query answering with data-tractable description logics. In: Proc. of Reasoning Web. pp. 218–307 (2015) 6. Botoeva, E., Konev, B., Lutz, C., Ryzhikov, V., Wolter, F., Zakharyaschev, M.: Inseparability and conservative extensions of description logic ontologies: A survey. In: Reasoning Web: Proceedings of 12th International Summer School. pp. 27–89 (2016) 7. Botoeva, E., Lutz, C., Ryzhikov, V., Wolter, F., Zakharyaschev, M.: Query-based entailment and inseparability for ALC ontologies. In: Proceedings of IJCAI. pp. 1001–1007 (2016) 8. Calı̀, A., Gottlob, G., Pieris, A.: Towards more expressive ontology languages: The query answering problem. Artif. Intell. 193, 87–128 (2012) 9. Calvanese, D., De Giacomo, G., Lembo, D., Lenzerini, M., Rosati, R.: Data com- plexity of query answering in description logics. Artificial Intelligence 195, 335–360 (2013) 10. Carral, D., Feier, C., Grau, B.C., Hitzler, P., Horrocks, I.: EL-ifying ontologies. In: IJCAR. pp. 464–479 (2014) 11. Chang, C.C., Keisler, H.J.: Model Theory, Studies in Logic and the Foundations of Mathematics, vol. 73. Elsevier (1990) 12. Eiter, T., Gottlob, G., Ortiz, M., Simkus, M.: Query answering in the description logic Horn-SHIQ. In: JELIA. pp. 166–179 (2008) 13. Feier, C., Lutz, C., Kuusisto, A.: Rewritability in monadic disjunctive datalog, mmsnp, and expressive description logics. In: ICDT (2017) 14. Hernich, A., Lutz, C., Ozaki, A., Wolter, F.: Schema.org as a description logic. In: Proceedings of IJCAI. pp. 3048–3054 (2015) 15. Hernich, A., Lutz, C., Papacchini, F., Wolter, F.: Dichotomies on ontology-mediated querying with the guarded fragment. In: Proceedings of PODS (2017) 16. Hustadt, U., Motik, B., Sattler, U.: Reasoning in description logics by a reduction to disjunctive datalog. J. Autom. Reasoning 39(3), 351–384 (2007) 17. Kaminski, M., Grau, B.C.: Computing horn rewritings of description logics ontolo- gies. In: Proceedings of IJCAI. pp. 3091–3097 (2015) 18. Kaminski, M., Nenov, Y., Grau, B.C.: Datalog rewritability of disjunctive datalog programs and non-horn ontologies. Artif. Intell. 236, 90–118 (2016) 19. Kazakov, Y.: Consequence-driven reasoning for Horn-SHIQ ontologies. In: Boutilier, C. (ed.) IJCAI. pp. 2040–2045 (2009) 20. Konev, B., Lutz, C., Wolter, F., Zakharyaschev, M.: Conservative rewritability of description logic tboxes. In: IJCAI. pp. 1153–1159 (2016) 21. Kontchakov, R., Lutz, C., Toman, D., Wolter, F., Zakharyaschev, M.: The combined approach to query answering in DL-Lite. In: Proc. of KR (2010) 22. Kontchakov, R., Zakharyaschev, M.: An introduction to description logics and query rewriting. In: Proc. of Reasoning Web. pp. 195–244 (2014) 23. Krisnadhi, A., Lutz, C.: Data complexity in the el family of dls. In: Proc. of DL (2007) 24. Krötzsch, M., Rudolph, S., Hitzler, P.: Complexity boundaries for Horn description logics. In: AAAI. pp. 452–457 (2007) 25. Lutz, C., Piro, R., Wolter, F.: Description logic tboxes: Model-theoretic characteri- zations and rewritability. In: IJCAI (2011) 26. Lutz, C., Wolter, F.: Deciding inseparability and conservative extensions in the description logic EL. J. Symb. Comput. 45(2), 194–228 (2010) 27. Lutz, C., Wolter, F.: Non-uniform data complexity of query answering in description logics. In: Proc. of KR. AAAI Press (2012) 28. Mugnier, M., Thomazo, M.: An introduction to ontology-based query answering with existential rules. In: Proc. of Reasoning Web. pp. 245–278 (2014) 29. Ortiz, M., Rudolph, S., Simkus, M.: Query answering in the Horn fragments of the description logics SHOIQ and SROIQ. In: IJCAI. pp. 1039–1044 (2011) 30. Poggi, A., Lembo, D., Calvanese, D., Giacomo, G.D., Lenzerini, M., Rosati, R.: Linking data to ontologies. J. Data Semantics 10, 133–173 (2008) 31. Schaerf, A.: On the complexity of the instance checking problem in concept languages with existential quantification. J. of Intel. Inf. Systems 2, 265–278 (1993)