Horn Rewritability vs PTime Query Evaluation for Description Logic TBoxes

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 quanti er 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 identi cation 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 de ned fragments of expressive DLs that fall within the Hornfragment of rst-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 ontologymediated querying where it typically su ces 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 CQinseparable 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 satis es 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 a ecting 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 quanti ers 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 rst 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 i 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 di erence 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 ].

Preliminaries

We use the notation from [ 2 ]. Let NC and NR be countably in nite 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 de ne 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 E LI concepts which are constructed using >, u, and 9r:C, r a role.

An ABox A is a non-empty nite set of assertions of the form A(a) and r(a; b) with A 2 NC, r 2 NR, and a; b individual names.

Interpretations I and the extension CI of a concept C are de ned as usual. An interpretation I satis es a CI C v D if CI DI , an RI r v s if rI sI , an assertion A(a) if a 2 AI , an assertion r(a; b) if (a; b) 2 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 satis es all inclusions and assertions in T and I is a model of an ABox A if it satis es all assertions in A. We call an ABox A satis able 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 9r:C and 8r:C in it; thus 9r:A has depth 1 and 9r:8r: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 ::= > j ? j A j :A j R u R0 j :L t R j 9r:R j 8r:R

L; L0 ::= > j ? j A j L u L0 j L t L0 j 9r:L A Horn-ALCHIF TBox is a nite set of Horn-ALCI CIs, RIs, and functionality assertions. Note that there are several alternative ways to de ne Horn-DLs [ 16, 24, 12, 19 ], our de nition is from [27]. The results in this paper remain valid under the alternative de nitions.

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 j= q(a), if I j= 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 j= 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 satis ability and subsumption, TBoxes are often normalized to depth 1 in a pre-processing step. Since we are universally quantifying over all queries when de ning 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 HornTBox, 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 de ned by setting I1 I2 =

I1

I2 AI1 I2 = f(d1; d2) j d1 2 AI1 ; d2 2 AI2 g rI1 I2 = f((d1; d2); (e1; e2)) j (d1; e1) 2 rI1 ; (d2; e2) 2 rI2 g 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 j= q(a) i T2; A j= 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 = f9r:(A u :B u :E) v 9r:(:A u :B u :E)g: It is easy to see that for any CQ q(x), ABox A, and tuple a of individuals from A, we have T ; A j= q(a) i ;; A j= 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 = f0; 1g, rIi = f(0; 1)g, and AIi = f1g for i = 1; 2, but BI1 = f1g, EI1 = ;, BI2 = ;, and EI2 = f1g. 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 satis able 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 j= q(a) i I j= q(a).

T has the disjunction property for CQs if for any ABox A, CQs q1; : : : ; qn and

tuples a1; : : : ; an of individuals in A, T ; A j= W1 i n qi(ai) implies that there is a j with T ; A j= 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 j= q(a) i A j= (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 di erent 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 = f( 3r) v Ag. 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 j= ( 3r) v A since, for A = fr(a; b1); r(a; b2); r(a; b3)g, we have T ; A j= A(a) and thus T 0; A j= A(a). We also have T 0 6j= ( 2r) v A since, for A = fr(a; b1); r(a; b2)g, we have T ; A 6j= A(a) and thus T 0; A 6j= A(a). Take a model I of T 0 with d 2 ( 2r)I but d 62 AI . Then (d; d) 2 ( 3r)I I and (d; d) 62 AI I . Thus I I is not a model of T 0. tu 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 9s1:(B1 u B2) v 9r:> 9s1:> u 9s2:> v 8s1:B1 u 8s2:B2 9s1:> u 9s2:> v B t 9r:> We rst 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 nal 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 9r:> 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 2 f1; 2g. 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 satis able 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 = fs1(a; b1); s2(a; b2)g;

A2 = fs1(a; b); s2(a; b)g: Then T ; A1 j= B(a) and T ; A2 j= 9r:>(a), but T ; A1 6j= 9r:>(a) and T ; A2 6j= 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 62 (9r:>)I1 and a model I2 of T 0 and A2 with a 62 BI2 . Then I1 I2 is a model of A1 (for a identi ed with (a; a), b1 with (b1; b) and b2 with (b2; b)). However, we do not have a 2 BI1 I2 and since T 0; A1 j= B(a) it follows that I1 I2 is not a model of T 0. tu

Horn Rewritability in ALCHI F We introduce a mild restriction on ALCHIF TBoxes regarding the interaction between RIs and functionality assertions and show that this restriction is su cient 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 2 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-inseparable 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 E LI-concept of depth 1;

2. D is a disjunction of { concept names; { concepts 9r:E with E a conjunction of literals; { concepts 8r: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) 2 F : { any 9r:D0 in D contains only positive literals; { if there exists an 9r:C0 in C, then this is the only occurrence of r in C v D; { if there exists a 8r: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 jT j.

Example 2. The TBox T from Example 1 can be transformed into the TBox

T 0 = f9r:A v 9r:(:A u :B u :E) t 8r:(A ! B t E)g; which is in normal form. If r is functional, one obtains f> v 8r:(A ! B t E)g. We now identify a basic yet crucial property of ALCHIF vf TBoxes T . For any E LI concept C of depth 1 that contains at most one conjunct of the form 9r:C0 per functional role r one can de ne in a straightforward way a tree-shaped ABox AC of depth 1 with root C that corresponds to C. For example, when C = 9r:> u 9s:(A u B) then AC = fr( C ; b1); s( C ; b2); A(b2); B(b2)g. Then one can prove the following: Lemma 3. For every ALCI-concept D, T j= C v D i T ; AC j= 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 6j= CA1 v B, but T ; A1 j= 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 8r:E is a universal restriction with E a disjunction of literals that contains at least one positive literal, then a Horn specialization of 8r:E is a concept 8r:E0 where E0 is obtained from E by dropping all but one positive literal. Note that any Horn specialization can be written in the form 8r:(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 9r:neg(E) such that there is a CI in T whose right-hand side contains a disjunct 8r:E.

A set S LT is a trigger for a CI C v D 2 T if S contains all top-level conjuncts of C and all 9r:neg(E) with 8r:E a disjunct of D. For a trigger S, we denote by CS the conjunction of all concept names in S, all existential restrictions 9r:C0 2 S with r not functional, and all 9r:(C1u uCn) where r is functional and C1; : : : ; Cn is the set of all concepts such that 9r:Ci 2 S. For each CI C v D 2 T and trigger S for it, we de ne a set Horn(C v D; S) of Horn-ALCHIF vf CIs. As a special case, Horn(C v D; S) is fCS v ?g if T j= 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 = 8r:(A1 u u An ! A) a Horn restriction of some universal restriction in D; { CS v 9r:pos(E) with 9r:E an existential restriction in D such that T 6j=

CS v :9r:E.

De ne a Horn-ALCHIF TBox Thorn as the union of all functionality assertions and RIs in T and

[ CvD2T ; S trigger for CvD

Horn(C v D; S) Observe that, by construction, T j= Thorn.

Example 3. For the TBox T 0 from Example 2 we have LT 0 = f9r:A; 9r:>g and thus f9r:Ag is the only trigger for 9r:A v 9r:(:Au:B u:E)t8r:(A ! B tE) up to logical equivalence. Thus, Th0orn = f9r:A v 9r:>g 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 2 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 2 T and a trigger S for C v D such that Horn(C v D; S) = ;.

Let A1; : : : ; Ak, 9r1:E1; : : : ; 9rn:En, and 8s1:F1; : : : ; 8sm:Fm be the disjuncts of D such that T 6j= CS v :9ri: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 9si:neg(Fi) in CS. By Lemma 3, we have: T ; ACS j=

_ Ai(a0) _ _ 9ri:pos(Ei)(a0) _ i=1::k i=1::n _

_ i=1::m A2pos(Fi)

A(ai): 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 j= CS v Ai; { if F (a) = A(ai) for some A 2 pos(Fi), then T j= CS v 8si:(neg(Fi) ! A); { if F (a) = 9ri:pos(Ei)(a0), then T j= CS v 9ri:pos(Ei).

In each case, we obtain an

2 Horn(C v D; S) and thus derive a contradiction.

(2.) ) (3.). Assume (2.) holds. It su ces to show that for every ABox A the following holds: if A is satis able 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) 2 rI and r v s 2 T , then add (d; e) to sI ; 2. if d 2 CI and C v A 2 Thorn, then add d to AI ; 3. if d 2 CI and C v R 2 Thorn for R = 8r:(A1 u u An ! A), then add e to

AI whenever (d; e) 2 rI and e 2 (A1 u u An)I . 4. if d 2 CI and C v 9r:pos(E) 2 Thorn then (i) if r is functional and there exists e with (d; e) 2 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; 9r:E) with 9r:E on the right hand side of a CI in Thorn.

The element e required by this rule is called the witness for 9r: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 satis able w.r.t. Thorn (here one uses that T does not contain any functional roles s with T j= 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 2 U and assume that the chase introduces e as a witness for 9r:E at d. We say that this witness has been invalidated if e 2= EU . Observe that if r is a functional role then for any C v 9r:pos(E) 2 Thorn we have E = pos(E). Thus for functional roles r no witnesses for 9r:E can be invalidated. For an interpretation I and d 2 I we denote by eltpTU (d) the set of all F 2 LT such that d 2 F I . Claim 1. If the witness for 9r:E at d was invalidated, then Thorn j= CS v :9r:E for S = eltpTU (d).

For the proof of Claim 1, denote by ACS the ABox with root S corresponding 9r:pos(E) the extension of ACS with a fresh individual e and to CS. Denote by ACS fresh assertions r( F ; e) and A(e) for A 2 pos(E). We now apply the chase 9r:pos(E) rather that A and obtain a materialization U 0 procedure for Thorn to ACS of A9CrS:pos(E) and Thorn. Using the fact that the CIs of Thorn have depth 1 and the condition that the witness for 9r:E at d was invalidated in the chase applied to 9r:pos(E) as well. Thus e 62 EU0 A one can readily show that it is invalidated in ACS and it follows with Lemma 3 that Thorn j= CS v :9r:E.

Claim 2. U is a model of T .

Let C v D 2 T and d 2 CU . We show that d 2 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 2 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 j= CS v A. Then CS v A 2 Thorn and so d 2 AU . Thus d 2 DU and we have derived a contradiction. 2. there is a universal restriction R = 8r:(A1 u u An ! A) that is a Horn restriction of some universal restriction in D such that T j= CS v R. Then CS v R 2 Thorn and so d 2 RU . Thus d 2 DU and we have derived a contradiction. 3. there is an 9r:E in D such that T j= CS v 9r:pos(E) and T 6j= CS v :9r:E.

Then there exists e 2 U with (d; e) 2 rU such that e 2 pos(E)U . By Claim 1, the witness e for 9r:E at d was not invalidated. Thus d 2 (9r:E)U . Hence d 2 DU and we have derived a contradiction.

This nishes the proof of Theorem 6. tu The following example shows that Thorn can be of exponential size in jT j even if redundant CIs are removed.

Example 4. Let T n contain

Bi v 8s:Ai ^ Bi v 8s:Ai 9r:> v 9s:> 9r:> v A t 1 ti n 9s::Ai where 1 i n. The TBox Thnorn is obtained from Tn by replacing the nal CI by the set of CIs

9r:> u 1 ui n Ci v A where Ci 2 fBi; B^ig. Then Thnorn and T n are CQ-inseparable and Thnorn is of exponential size in jT nj.

n Clearly, the TBoxes Thorn can be equivalently expressed by Horn-TBoxes of polynomial size in jT nj 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 HornALCHIF 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 CQinseparable rewritability into Horn-TBoxes is decidable and ExpTime-complete for such ALCHIF TBoxes since it is shown in [ 15 ] that deciding whether CQevaluation 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 di cult to see that CQ-evaluation is coNPhard 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 quali ed 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 Andre 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. 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. Krotzsch, 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 characterizations 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 quanti cation. J. of Intel. Inf. Systems 2, 265{278 (1993)

References

1. Artale , A. , Calvanese , D. , Kontchakov , R. , Zakharyaschev , M.: The DL-Lite family and relations . J. of Arti cal 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 containment 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 complexity of query answering in description logics . Arti cial 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 ontologies . 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 )