Conservative Rewritability of Description Logic TBoxes: First Results

Abstract

We want to understand when a given TBox T in a description logic L can be rewritten into a TBox T 0 in a weaker description logic L0. Two notions of rewritability are considered: model-conservative rewritability (T 0 entails T and all models of T can be expanded to models of T 0) and L-conservative rewritability (T 0 entails T and every L-consequence of T 0 in the signature of T is a consequence of T ) and investigate rewritability of TBoxes in ALCI to ALC, ALCQ to ALC, ALC to EL?, and ALCI to DL-Litehorn. We compare conservative rewritability with equivalent rewritability, give model-theoretic characterizations of conservative rewritability, prove complexity results for deciding rewritability, and provide some rewriting algorithms.

-

Over the past 30 years, a multitude of di erent description logics (DLs) have been designed, investigated, and used in practice as ontology languages. The introduction of new DLs has been driven both by the need for additional expressive power (such as transitive roles in the 1990s) and by applications that require e cient reasoning of a novel type (such as ontology-based data access in the 2000s). While the resulting exibility in choosing DLs has had the positive e ect of making DLs available for a large number of domains and applications, it has also led to the development of ontologies with language constructors that are not really required to axiomatize their knowledge. For a constructor to be `not required' can mean di erent things here, ranging from the high-level `this domain can be represented in an adequate way in a weaker DL' to the very concrete `this ontology is logically equivalent to an ontology in a weaker DL'. In this paper, we take the latter understanding as our starting point. Equivalent rewritability of a given DL ontology (TBox) to a weaker DL has been investigated in [ 17 ], where model-theoretic characterizations and the complexity of deciding rewritability were investigated. For example, equivalent rewritability of an ALC TBox to an E L? TBox has been characterized in terms of preservation under products and global equisimilations, and a NExpTime upper bound for deciding equivalent rewritability has been established. Equivalent rewritability is a very strong notion, however, that appears to apply to a very small number of real-world TBoxes. A more practically relevant notion we propose in this paper is conservative rewritability, which allows one to use new concept and role names when rewriting a given ontology into a weaker DL. In this case, we clearly cannot demand that the new TBox is logically equivalent to the original one, but only that it entails the original TBox. To avoid uncontrolled additional consequences of the new TBox, we can also require that (i ) it does not entail any new consequences in the language of the original TBox, or even that (ii ) every model of the original TBox can be expanded a model of the new TBox. The latter type of conservative extension is known as model-conservative extension [ 16 ], and we call a TBox T model-conservatively L-rewritable if a model-conservative rewriting of T in the DL L exists. The former type of conservative extension is known as a language-conservative extension or deductive conservative extension [ 12 ] and, given a DL L in which T is formulated and a weaker DL L0, we call T L-conservatively L0-rewritable if there is a TBox T 0 in L0 such that T 0 has the same L-consequences as T in the signature of T . Model-conservative rewritability is the more robust notion as it is language-independent and does not only leave unchanged the entailed concept inclusions of the original TBox but also, for example, certain answers if the ontologies are used to access data.

The main result of this paper is that there are important DLs for which model-conservative and L-conservative rewritability can be transparently characterized, e ectively decided, and for which rewriting algorithms can be designed. This is in contrast to the undecidability of the problem whether one TBox is a model-conservative extension of another one even for weak DLs such as E L [ 18, 16 ]. In particular, we show that, given an ALCI TBox, one can compute in polynomial time its model-conservative ALC-rewriting provided that such a rewriting exists, which can be decided in ExpTime. We characterize model-conservative ALC-rewritability in terms of preservation under generated subinterpretations and show that ALCI-conservative ALC-rewritability coincides with model-conservative one. For ALCQ TBoxes, we show that modelconservative ALC-rewritability coincides with equivalent rewritability, but is di erent from ALCQ-conservative rewritability. The latter can be characterized using bounded morphisms, and all these notions of rewritability are decidable in 2ExpTime. Unlike the ALCI case, we currently do not have polynomial rewritings for ALCQ TBoxes. As to rewritability from ALCI to DL-Litehorn, we observe that all our notions of rewritability coincide and are ExpTimecomplete. In contrast, for rewritability from ALC to E L? they are all distinct and, in fact, rather intricate and di cult to analyse. We prove decidability of model-conservative rewritability and give necessary semantic conditions for both ALC-conservative and model-conservative E L?-rewritability.

Related work. Conservative rewritings of TBoxes are ubiquitous in the DL research. For example, many rewritings of TBoxes into normal forms are modelconservative [ 14, 4 ]. Regarding rewritability of TBoxes into weaker DLs, the focus has been on polynomial satisfability preserving rewritings as a pre-processing step to reasoning [ 11, 9, 8 ] or to prove complexity results for reasoning [ 10 ]. Such rewritings are mostly not conservative. There has been signi cant work on rewritings of ontology-mediated queries (pairs of ontologies and queries), which preserve their certain answers, into datalog or ontology-mediated queries based on weaker DLs [ 13, 5 ]. It seems, however, that this problem is di erent from TBox conservative rewritability. In [ 2 ], the expressive power of DLs and corresponding notions of rewritability are introduced based on a variant of model-conservative extension, and the relationship to L-conservative extensions is discussed.

For omitted proofs, see http://cgi.csc.liv.ac.uk/ frank/publ/publ.html. 1

Conservative Rewritability We consider the standard description logics ALC, ALCI, ALCQ, EL?, and DL-Litehorn [ 3, 4, 7, 1 ], where EL? is EL extended with the concept ?, and DL-Litehorn is DL-Litecore extended with conjunctions of basic concepts on the left-hand side of concept inclusions. As usual, the alphabet of DLs consists of countably in nite sets NC of concept names and NR of role names. By a signature, , we mean any set of concept and role names. The signature sig(T ) of a TBox T is the set of concept and role names occurring in T .

Before introducing our notions of conservative rewritability, we remind the reader of a simpler notion of TBox rewritability. Suppose L and L0 are DLs; we typically assume that L is more expressive than L0.

De nition 1 (equivalent L-to-L0 rewritability). An L0 TBox T 0 is called an equivalent L0-rewriting of an L TBox T if T j= T 0 and T 0 j= T (in other words, if T and T 0 have the same models). An L TBox is called equivalently L0-rewritable if it has an equivalent L0-rewriting.

Equivalent L-to-L0 rewritability has been studied in [ 17 ], where semantic characterizations are given and complexity results for deciding equivalent rewritability are obtained for various DLs L and L0. For example, if L is ALCI or ALCQ and L0 is ALC, then an L TBox T is equivalently L0-rewritable just in case its class of models is preserved under global bisimulations, which are de ned as follows. Given interpretations Ii = ( Ii ; Ii ), for i = 1; 2, and a signature , we call a relation S I1 I2 a -bisimulation between I1 and I2 if { for any A 2 , whenever (d1; d2) 2 S then d1 2 AI1 i d2 2 AI2 ; { for any r 2 and (d1; d2) 2 S, if (d1; e1) 2 rI1 then there is e2 such that (e1; e2) 2 S and (d2; e2) 2 rI2 , if (d2; e2) 2 rI2 then there is e1 such that (e1; e2) 2 S and (d1; e1) 2 rI1 . S is a global -bisimulation between I1 and I2 if I1 is the domain of S and I2 its range. I1 and I2 are globally -bisimilar if there is a global -bisimulation between them, in which case we write I1 ALC I2. For d1 2 I1 and d2 2 I2 , we say that (I1; d1) is -bisimilar to (I2; d2) if there is a -bisimulation S between I1 and I2 such that (d1; d2) 2 S. If = NC [ NR, we omit , write I1 ALC I2 and say simply `(global) bisimulation.' Example 1. The ALCI TBox f9r :B v Ag can be equivalently rewritten to the ALC TBox fB v 8r:Ag. However, the ALCI TBox T = f9r :B u 9s :B v Ag is not equivalently ALC-rewritable. Indeed, the interpretation on the right-hand side in the picture below is a model of T and globally bisimilar to the interpretation on the left-hand side, which is not a model of T .

r

s We now introduce two subtler notions of TBox rewritability, which allow the use of fresh concept and role names in rewritings. For an interpretation I and signature , the -reduct of I is the interpretation Ij coinciding with I on the names in and having XIj = ; for all X 2= . We say that interpretations I and J coincide on and write I = J if the -reducts of I and J coincide. A TBox T 0 is a model-conservative extension of T if an interpretation I is a model of T just in case there is a model I0 of T 0 such that I =sig(T ) I0. De nition 2 (model-conservative L-to-L0-rewritability). An L0 TBox T 0 is called a model-conservative L0-rewriting of an L TBox T if T 0 is a modelconservative extension of T . An L TBox T is model-conservatively L0-rewritable if a model-conservative L0-rewriting of T exists.

Clearly, any equivalent L0-rewriting of a TBox T is also a model-conservative L0-rewriting of T . The next example shows that the converse does not hold. Example 2. The ALCI TBox T = f9r :B u 9s :B v Ag from Example 1 is model-conservatively ALC-rewritable to

T 0 = fB v 8r:B9r :B; B v 8s:B9s :B; B9r :B u B9s :B v Ag; where B9r :B, B9s :B are fresh concept names.

A TBox T 0 is called an L-conservative extension of T if T 0 j= T and T 0 j= C v D implies T j= C v D, for every L-concept inclusion C v D formulated in sig(T ). De nition 3 (L-conservative L0-rewritability). An L0 TBox T 0 is called an L-conservative L0-rewriting of an L TBox T if T 0 is an L-conservative extension of T . An L TBox T is L-conservatively L0-rewritable if an L-conservative L0rewriting of T exists.

It should be clear that every model-conservative L0-rewriting of an L TBox T is also an L-conservative L0-rewriting of T . The next example shows that the converse implication does not hold.

Example 3. The ALCQ TBox T = fA v 2 r:Bg is ALCQ-conservatively ALCrewritable to T 0 = fA v 9r:C; A v 9r:D; C v :D; C t D v Bg; where C and D are fresh concept names. However, T 0 is not a model-conservative rewriting of T because the model of T shown below is not the sig(T )-reduct of any model of T 0. Note that T is not equivalently ALC-rewritable.

B r A r

B A r

B r A In our examples so far, we have used fresh concept names but no fresh role names. This is no accident: it turns out that, for the DLs considered in this paper, fresh role names in conservative rewritings are not required. More precisely, we call a model-conservative or L-conservative L0-rewriting T 0 of T a model-conservative or, respectively, L-conservative L0-concept rewriting of T if sigR(T ) = sigR(T 0), where sigR(T ) is the set of role names in T .

Say that a DL L re ects disjoint unions if, for any L TBox T , whenever the disjoint union Si2I Ii of interpretations Ii is a model of T , then each Ii, i 2 I, is also a model of T . All the DLs considered in this paper re ect disjoint unions. Theorem 1. Let L be a DL re ecting disjoint unions, T an L TBox, and let L0 2 fALC; E L?; DL-Litehorng. Then T is model-conservatively (or L-conservatively ) L0-rewritable if and only if it is model-conservatively (or, respectively, L-conservatively ) L0-concept rewritable. 2

ALCI -to-ALC Rewritability

Equivalent ALCI-to-ALC rewritability was studied in [ 17 ], where the characterization in terms of global bisimulations was used to design a 2ExpTime algorithm for checking this property. Here, we give a characterization of model-conservative ALC rewritability of ALCI TBoxes in terms of generated subinterpretations and use it to show that (i ) model-conservative ALCI-to-ALC rewritings are of polynomial size and can be constructed in polynomial time (if they exist), and that (ii ) deciding model-conservative ALCI-to-ALC rewritability is ExpTimecomplete. We also observe that ALCI-conservative ALC-rewritability coincides with model-conservative rewritability.

We remind the reader that an interpretation I is a subinterpretation of an interpretation J if I J , AI = AJ \ I for all concept names A, and rI = rJ \ ( I I ) for all role names r. I is a generated subinterpretation of J if, in addition, whenever d 2 I and (d; d0) 2 rJ , r a role name, then d0 2 I . We say that a TBox T is preserved under generated subinterpretations if every generated subinterpretation of a model of T is also a model of T . As well known, every ALC TBox is preserved under generated subinterpretations.

Suppose we want to nd a model-conservative ALC-rewriting of an ALCI TBox T . Without loss of generality, we assume that T = f> v CT g and CT is built using :, u and 9 only. Let sub(T ) be the closure under single negation of the set of (subconcepts) of concepts in T . For every role name r in T , we take a fresh role name r and, for every 9r:C in sub(T ) (where r is a role name or its inverse), we take a fresh concept name B9r:C . Denote by D] the ALCconcept obtained from any D 2 sub(T ) by replacing every top-most occurrence of a subconcept of the form 9r:C in it with B9r:C . Now, let T y be an ALC TBox comprised of the following concept inclusions, for r 2 NR: > v CT] , C] v 8r:B9r:C ; B9r:C 9r:C]; for every 9r:C 2 sub(T ); C] v 8r:B9r :C ;

B9r :C for every 9r :C 2 sub(T ): Clearly, T y can be constructed in polynomial time in the size of T . Theorem 2. An ALCI TBox T is model-conservatively ALC-rewritable i T is preserved generated subinterpretations. Moreover, if T is model-conservatively ALC-rewritable, then T y is its model-conservative ALC-rewriting. It is now easy to show that model-conservative ALCI-to-ALC rewritability is decidable in ExpTime. By Theorem 2, this amounts to deciding whether T y is a model-conservative extension of T . In general, this is an undecidable problem. It is, however, easy to see that, for every model I of T , there is a model I0 of T y such that I =sig(T ) I0. It thus remains to decide whether every interpretation I with I =sig(T ) I0, for some model I0 of T y, is a model of T . In other words, this means to decide whether T y j= T , which can be done in ExpTime. A matching lower bound is easily obtained by reducing satis ability in ALC. Corollary 1. The problem of deciding model-conservative ALCI-to-ALC rewritability is ExpTime-complete.

ALCI-conservative ALC-rewritability of ALCI TBoxes coincides with modelconservative ALC-rewritability. This can be proved using the characterization via subinterpretations and robustness under replacement of ALCI TBoxes, an important property in the context of modular ontology design [15, Theorem 4]. Theorem 3. An ALCI TBox T is ALCI-conservatively ALC-rewritable i T is model-conservatively ALC-rewritable. 3

ALCQ-to-ALC Rewritability

Equivalent ALCQ-to-ALC rewritability was characterized in [ 17 ] in terms of preservation under global bisimulations. Below, we use this characterization to give a 2ExpTime algorithm for checking equivalent ALC-rewritability.

We rst prove a characterization of ALCQ-conservative ALC-rewritability in terms of preservation under inverse bounded morphisms and use it to show that one can (i ) decide ALCQ-conservative ALC-rewritability in 2ExpTime and (ii ) construct e ectively an ALCQ-conservative rewriting if it exists. We also show that, unlike ALCI-to-ALC-rewritability, model-conservative ALCrewritability of ALCQ TBoxes coincides with equivalent rewritability.

A bounded -morphism from an interpretation I1 to an interpretation I2 is a global -bisimulation S between I1 and I2 such that S is a function from

I1 to I2 . A class K of interpretations is preserved under inverse bounded morphisms if whenever there is a bounded -morphism from an interpretation I1 to some I2 2 K, then I1 2 K. The following lemma provides the fundamental property of bounded morphisms: Lemma 1. Suppose f : I1 ! I2 is a bounded -morphism, where I2 is a model of an ALC TBox T and sigR(T ) . Then there is J1 j= T such that J1 = I1. Proof. We de ne J1 in the same way as I1 except that BJ1 := f 1(BI2 ) for all concept names B 2 sig(T1) n . Then f is a bounded sig(T )-morphism from J1 to I2. Thus, J1 is a model of T since I1 is a model of T . o An interpretation I is a directed tree interpretation if rI \ sI = ;, for r 6= s, and the directed graph with nodes I and edges E de ned by setting (d; d0) 2 E i (d; d0) 2 Sr2NR rI is a directed tree. We start our investigation with the observation that ALCQ-conservative ALCQ-to-ALC rewritability can be regarded as a principled approximation of model-conservative rewritability: Lemma 2. An ALC TBox T 0 is an ALCQ-conservative rewriting of an ALCQ TBox T i T 0 is a model-conservative rewriting of T over the class of directed tree interpretations of nite outdegree.

Suppose we want to nd an ALCQ-conservative ALC-rewriting of an ALCQ TBox T . Without loss of generality, we assume that T is of the form f> v CT g and that CT is built using :, u, (> n r C) only. Construct a TBox T y as follows. Take fresh concept names BD; B1D; : : : ; BnD for every D = (> n r C) 2 sub(T ). We use to denote sig(T ) extended with all fresh concept names of the form BiD. For each C 2 sub(T ), C] denotes the ALC-concept that results from C by replacing all top-most occurrences of any D = (> n r C) in T with BD. Now, de ne T y to be the in nite TBox that consists of the following inclusions: { > v CT] , {{ BBDD v 9r:(C] u B1D) u u 9r:(C] u BnD),

i v :BjD, for i 6= j, and { for all ALC-concepts C1; : : : ; Cn in and all D = (> n r C) 2 sub(T ), 1 ui n(9r:(C] u Ci u ju6=i :Cj])) v BD: ] The next theorem characterizes ALCQ-conservative ALC-rewritability. Theorem 4. An ALCQ TBox T is ALCQ-conservatively ALC-rewritable i T is preserved under inverse bounded sig(T )-morphisms. Moreover, if T is ALCQconservatively ALC-rewritable, then T y is an (in nite) rewriting. The semantic characterization of Theorem 4 can be employed to prove the following complexity result using a type elimination argument. We assume that numbers in number restrictions are given in unary.

Theorem 5. For ALCQ TBoxes, ALCQ-conservative ALC-rewritability is decidable in 2 ExpTime.

It follows that, given an ALCQ TBox T , one can rst decide ALCQ-conservative ALC-rewritability and then, in case of a positive answer, e ectively construct a rewriting by going through the nite subsets of T y in a systematic way until a nite T 0 T y with T 0 j= T is reached. By compactness, such a set T 0 exists.

We nally show that every model-conservatively ALC-rewritable ALCQ TBox is equivalently ALC-rewritable.

Theorem 6. An ALCQ TBox is model-conservatively ALC-rewritable i it is equivalently ALC-rewritable, which is decidable in 2 ExpTime. 4

ALCI -to-DL-Litehorn and ALC-to-E L? Rewritability We rst observe that all notions of rewritability introduced in this paper coincide in the case of ALCI-to-DL-Litehorn rewritability. Deciding rewritability is ExpTime-complete in all cases since deciding equivalent ALCI-to-DL-Litehorn rewritability is ExpTime-complete [ 17 ]: Theorem 7. For ALCI TBoxes, equivalent DL-Litehorn-rewritability, modelconservative DL-Litehorn-rewritability, and ALCI-conservative DL-Litehorn-rewritability coincide and are ExpTime-complete.

We now provide separating examples for all three notions of ALC-to-E L? rewritability and then prove decidability of model-conservative E L?-rewritability. While we have not yet been able to nd purely model-theoretic characterizations of model- and ALC-conservative E L?-rewritability, we then give necessary model-theoretic conditions for these two notions of rewritability.

Equivalent ALC-to-E L? rewritability has been characterized in [ 17 ] in terms of preservation under products and global equisimulations. A simulation between interpretations I and J is a relation S I J such that, for any A 2 NC, r 2 NR and (d1; d2) 2 S, if d1 2 AI1 then d2 2 AI2 , and if (d1; e1) 2 rI then there exists e2 with (e1; e2) 2 S and (d2; e2) 2 rJ . (I; d) is simulated by (J ; e) if there is a simulation S between I and J such that (d; e) 2 S. Interpretations I and J are globally equisimilar if, for any d 2 I , there exists e 2 J such that (I; d) is simulated by (J ; e) and (J ; e) is simulated by (I; d). According to [17, Theorem 17], an ALC TBox is equivalently E L?-rewritable if its models are preserved under products and global equisimulations.

Example 4. The TBox T = f9r:A u 9r:B u 8r:(A t B) v E t F; A u B v ?g is not equivalently E L?-rewritable because its models are not preserved under global equisimulations. Indeed, the interpretation I shown below is clearly a model of T . However, by removing the rightmost r-arrow from I, we obtain an interpretation which is globally equisimilar to I but not a model of T .

A r

B r r

On the other hand, the EL? TBox

f9r:A u 9r:B v 9r:G; 9r:(G u A) v E; 9r:(G u B) v F; A u B v ?g is easily seen to be an ALC-conservative E L? rewriting of T . We now show that T is not model-conservatively E L?-rewritable. For suppose T has such a rewriting T 0 given in standard normal form (with inclusions of the form A1 u : : : u An v B, 9r:B v A, or A v 9r:B where A1; : : : ; An; A; B 2 NC [ f?g). Consider the model I of T depicted below, and let I0 be a model of T 0 such that I =sig(T ) I0.

A r E a x r b y

B r F Let J be the same as I0 except that x; y 2 M J i both x 2 M I0 and y 2 M I0 , for every M 2 NC. Since x 2= EJ and y 2= F J , J is not a model of T 0. Since the restriction of I0 to fa; bg is a model of T 0, and the restrictions of I0 to fa; b; xg and fa; b; yg coincide, there is (C v D) 2 T 0 such that x; y 2 CJ but x; y 62 DJ . As I0 is a model of T 0, which is in standard normal form, and by the de nition of J , D must be a concept name. Since clearly x; y 2 CI0 , we must also have x; y 2 DI0 , and so x; y 2 DJ , which is a contradiction.

The following modi ed version of T

Tm = f9r:A u 9r:B u 8r:(A t B) v 9r:(A u E) t 9r:(B u F ); A u B v ?g is not equivalently E L?-rewritable, but has a model-conservative E L?-rewriting Tm0 = f9r:A u 9r:B v 9r:M; 9r:(M u A) v 9r:(M u E);

9r:(M u B) v 9r:(M u F ); A u B v ?g: The di erence from the previous example is that if d is an instance of 9r:Au9r:B, then we can place the `marker' M onto an r-successor of d which is either in A u E or in B u F , whereas in the previous example the decision on where to put the `marker' G was not determined by the r-successors of d but by d itself. We now prove that if there exists an E L?-rewriting of an ALC TBox T , then there is one without any `recursion' for the newly introduced symbols. Let = sig(T ). We say that an E L? TBox T 0 is in -layered form of depth n if there are mutually disjoint sets 0; : : : ; n of concept names such that i \ = ; (0 i n) and the inclusions of T 0 take the following form, where r 2 : level i atom inclusions: A1 u u An v B, for A1; : : : ; An; B 2 level i right-atom inclusions: 9r:A v B for A 2 [ i+1, B 2 level i left-atom inclusions: A v 9r:B, for A 2 [ i, B 2 [ i [ f?g, [ i [ f?g, [ i+1 [ f?g.

The depth of a concept C is the maximal number of nestings of existential restrictions in C. The depth of a TBox is the maximal depth of its concepts. Lemma 3. If an ALC TBox T of depth n is model- (or ALC-) conservatively E L?-rewritable, then there exists a model- (respectively, ALC-) conservative E L?-rewriting T 0 of T in sig(T )-layered form of depth n.

We use Lemma 3 to prove decidability of model-conservative E L?-rewritability. An ALC ABox A is a nite set of assertions of the form C(a) and r(a; b), where C is an ALC concept and a; b are individual names. The set of individual names that occur in an ABox A is denoted by ind(A). When interpreting ABoxes, we adopt the standard name assumption: aI = a, for all a 2 ind(A). subnLe1t T be an ALC TBox of depth n > 0 (the case n = 0 is trivial). By (T ) we denote the closure under single negation of the set of subconcepts of concepts in T of depth at most n 1. By n 1(T ) we denote the set of maximal subsets t of subn 1(T ) that are satis able in a model of T . A T -ABox is an ABox such that tA(a) = fD j D(a) 2 Ag 2 n 1(T ) for all a 2 ind(A). Let A be a directed tree ABox of depth at most n (that is, all nodes in it are at distance n from the root). We say that A is n-strongly satis able w.r.t. T if there is a model I of A and T such that the rI -successors of aI , for every a 2 ind(A) of depth < n in A, coincide with the r-successors of a in A.

We now de ne inductively (T ; i)-bisimilarity relations i;T between pairs (A1; a1) and (A2; a2), where the Ai are T -ABoxes and ai 2 ind(Ai): { (A1; a1) 0;T (A2; a2) if tA1 (a1) = tA2 (a2); { (A1; a1) i+1;T (A2; a2) if (A1; a1) 0;T (A2; a2) and, for every r 2 sig(T ), if r(d1; e1) 2 A1 then there is r(d2; e2) 2 A2 such that (A1; e1) i;T (A2; e2), and vice versa.

For every i 0, one can determine a nite set ATi of nite directed tree T ABoxes A with root A and of depth i such that: { for every I j= T and every d 2

(A; A) 2 ATi;4 { every A 2 ATi is strongly i-satis able w.r.t. T .

I , (I; d) is (T ; i)-bisimilar to exactly one

We assume that all ABoxes in AT0; : : : ; ATn have mutually distinct roots. We de ne the canonical ABox AT with individuals f A j A 2 ATi; i ng as follows: { for Ai 2 ATi, Ai+1 2 ATi+1 and r 2 sig(T ), we have r( Ai+1 ; Ai ) 2 AT if there exists r( Ai+1 ; b) 2 Ai+1 such that the subtree of Ai+1 rooted at b is (i; T )-bisimilar to Ai; { for Ai 2 ATi and A 2 sig(T ), we have A( Ai ) 2 AT i A( Ai ) 2 Ai.

Note that AT is acyclic (but not a directed tree ABox).

Lemma 4. Let T be an ALC TBox of depth n. An EL? TBox T 0 in sig(T )layered form of depth n is a model-conservative EL?-rewriting of T i { T 0 j= T and { there exists A0 =sig(T ) AT such that, for all i = 0; : : : ; n, A0 satis es all level i inclusions in T 0 at all Ai with Ai 2 ATn i.

Theorem 8. Model-conservative EL?-rewritability of ALC TBoxes is decidable. Proof. Given an ALC TBox T , we rst construct the canonical ABox AT . If an EL? TBox T 0 in -layered form of depth n satis es the conditions of Lemma 4, then there exists such a TBox with at most 2jAT j distinct fresh concept names. As the number of such EL? TBoxes is nite, one can check for each of them whether the conditions of Lemma 4 are satis ed. o 4 Here we identify I with the ABox with assertions r(a; b), for (a; b) 2 rI, and D(a), for D 2 subn 1(T ) and a 2 DI.

We now give necessary conditions for ALC-conservative E L?-rewritability of ALC TBoxes. First, we still have the preservation under products: Theorem 9. Every ALC-conservatively E L?-rewritable ALC TBox is preserved under products.

Theorem 9 can be used to show that TBoxes such as fA v B t Eg are not ALC-conservatively E L?-rewritable. To separate equivalently rewritable TBoxes from ALC-conservatively rewritable TBoxes, we generalize the construction of Example 4. In that case, we removed an r-arrow (d0; d) from a tree-shaped model I of T and obtained a model that is globally equisimilar to the original model but not a model of T . It turns out that ALC-conservatively E L?-rewritable ALC TBoxes of depth 1 are preserved under the inverse of this operation. We say that (I; d) is 1-simulated by (J ; e) if (i ) d 2 AI i e 2 AJ , for all A 2 NC; (ii ) for all r 2 NR, if (e; e0) 2 rJ then there exists d0 with (d; d0) 2 rI and, for all A 2 NC, if e0 2 AJ then d0 2 AI ; (iii ) for all r 2 NR, if (d; d0) 2 rI then there exists e0 with (e; e0) 2 rJ and, for all A 2 NC, we have d0 2 AI i e0 2 AJ . Say that I is globally 1-simulated by J if, for every e 2 J , there exists d 2 I such that (I; d) is 1-simulated by (J ; e). An ALC TBox is preserved under 1-simulations if every interpretation that globally 1-simulates a model of T is a model of T .

Theorem 10. Every ALC-conservatively E L?-rewritable ALC TBox of depth 1 is preserved under global 1-simulations.

This result can be used to show, for example, that T = fA v 8r:Bg is not ALC-conservatively E L?-rewritable. For the interpretation below is not a model B r

A r of T , but by removing from it the rightmost r-arrow, we obtain an interpretation which is globally 1-simulated by J and is a model of T . It remains open whether preservation under products and global 1-simulations is su cient for an ALC TBox of depth 1 to be ALC-conservatively E L?-rewritable. 5

Conclusion Conservative rewritings of ontologies provide more exibility than equivalent rewritings and are more natural in practice. However, they are also technically much more challenging to analyse. For future work, we are particularly interested in better understanding conservative rewritings to EL and related logics. For example, can we nd transparent model-theoretic characterizations and explicit axiomatizations of the rewritten TBoxes? The results in Section 4 should provide a good starting point. Another challenging problem could be to investigate rewritability to OWL 2 QL|essentially DL-Litecore extended with role inclusions|which preserves answers to conjunctive queries over all possible ABoxes. (Recall [ 6 ] that conjunctive query inseparability for OWL 2 QL TBoxes is ExpTime-complete.)

References

1. Artale , A. , Calvanese , D. , Kontchakov , R. , Zakharyaschev , M.: The DL-Lite family and relations . Journal of Arti cial Intelligence Research 36 , 1 { 69 ( 2009 )

2. Baader , F. : A formal de nition for the expressive power of terminological knowledge representation languages . Journal of Logic and Computation 6 ( 1 ), 33 { 54 ( 1996 )

3. Baader , F. : The description logic handbook: Theory, implementation, and applications . Cambridge University Press, Cambridge ( 2007 )

4. Baader , F. , Brandt , S. , Lutz , C. : Pushing the EL Envelope . In: Proceedings of IJCAI . pp. 364 { 369 ( 2005 )

5. Bienvenu , M. , ten Cate , B. , Lutz , C. , Wolter , F. : Ontology-based data access: A study through disjunctive datalog, CSP, and MMSNP . ACM Transactions of Database Systems 39 ( 4 ), 33 ( 2014 )

6. Botoeva , E. , Kontchakov , R. , Ryzhikov , V. , Wolter , F. , Zakharyaschev , M. : Query inseparability for description logic knowledge bases . In: Proceedings of KR ( 2014 )

7. Calvanese , D. , De Giacomo , G. , Lembo , D. , Lenzerini , M. , Rosati , R. : Tractable reasoning and e cient query answering in description logics: The DL-Lite family . Journal of Automated Reasoning 39 ( 3 ), 385 { 429 ( 2007 )

8. Carral , D. , Feier , C. , Grau , B.C. , Hitzler , P. , Horrocks , I. : EL-ifying ontologies . In: Proceedings of IJCAR . pp. 464 { 479 ( 2014 )

9. Carral , D. , Feier , C. , Romero , A.A. , Grau , B.C. , Hitzler , P. , Horrocks , I.: Is your ontology as hard as you think? Rewriting ontologies into simpler DLs . In: Proceedings of DL . pp. 128 { 140 ( 2014 )

10. De Giacomo , G.: Decidability of Class-Based Knowledge Representation Formalisms . Ph.D. thesis , Universita di Roma ( 1995 )

11. Ding , Y. , Haarslev , V. , Wu , J.: A new mapping from ALCI to ALC . In: Proceedings of DL ( 2007 )

12. Ghilardi , S. , Lutz , C. , Wolter , F. : Did I damage my ontology? A case for conservative extensions in description logics . In: Proceedings of KR . pp. 187 { 197 ( 2006 )

13. Kaminski , M. , Grau , B.C. : Su cient conditions for rst-order and datalog rewritability in ELU . In: Proceedings of DL . pp. 271 { 293 ( 2013 )

14. Kazakov , Y. : Consequence-driven reasoning for horn SHIQ ontologies . In: Proceedings of IJCAI . pp. 2040 { 2045 ( 2009 )

15. Konev , B. , Lutz , C. , Walther , D. , Wolter , F. : Formal properties of modularisation . In: Modular Ontologies: Concepts , Theories and Techniques for Knowledge Modularization , pp. 25 { 66 ( 2009 )

16. Konev , B. , Lutz , C. , Walther , D. , Wolter , F. : Model-theoretic inseparability and modularity of description logic ontologies . Arti cial Intelligence 203 , 66 { 103 ( 2013 )

17. Lutz , C. , Piro , R. , Wolter , F. : Description logic TBoxes: Model-theoretic characterizations and rewritability . In: Proceedings of IJCAI ( 2011 )

18. Lutz , C. , Wolter , F. : Deciding inseparability and conservative extensions in the description logic EL . Journal of Symbolic Computation pp. 194 { 228 ( 2010 )

19. Lutz , C. , Wolter , F. : Foundations for uniform interpolation and forgetting in expressive description logics . In: Proceedings of IJCAI . pp. 989 { 995 ( 2011 )