Conservative Rewritability of Description Logic TBoxes

1 Introduction

Over the past 30 years, a multitude of description logics (DLs) have been designed, investigated, and used in practice as ontology languages. The introduction of new DLs has been driven by (i) the need for additional expressive power (e.g., transitive roles in the 1990s), and (ii) applications that require efficient reasoning of a novel type (e.g., ontology-based data access in the 2000s). While the resulting flexibility in choosing DLs has had the positive effect 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 represent their knowledge. A 'not required' constructor can mean different 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 a starting point. Equivalent rewritability of a DL ontology (TBox) to a weaker language has been investigated by Lutz, Piro, and Wolter [2011] who established model-theoretic characterizations in terms of (various types of) global bisimilations and applied them to the problem of deciding equivalent rewritability. However, equivalent rewritability seems to be an unnecessarily strong condition for multiple applications where fresh symbols can be used in rewritings.

Therefore, in this paper, we propose a more flexible notion of conservative rewritability that allows the use of fresh symbols in a rewriting T 0 of a given TBox T . We demand that T 0 entails T . On the other hand, to avoid uncontrolled additional consequences of T 0, we also require that (i) it does not entail any new subsumptions in the signature of T , or even that (ii) every model of T can be expanded to a model of T 0 . The latter type of conservative rewriting is known as model-conservative extension [Konev et al., 2013], and we call a TBox T model-conservatively L-rewritable if there is a model-conservative extension of T in the DL L. The former type is known as a subsumption or deductive conservative extension [Ghilardi, Lutz, and Wolter, 2006] and, given a DL L, an L TBox T and a weaker DL L0 , we call T subsumptionconservatively L0 -rewritable if there is a TBox T 0 in L0 such that T 0 entails the same L-subsumptions in the signature of T as T . Model-conservative rewritability is a more robust notion as it is language-independent and not only leaves unchanged the entailed subsumptions of the original TBox but also, for example, certain answers in case the ontologies are used to access data.

The main aim of this paper is to show that, for many important DLs, model- and subsumption-conservative rewritabilities can be characterized in terms of natural model-theoretic preservation conditions. In fact, the role played by global bisimilations for equivalent rewritability is now played by generated subinterpretations and p-morphisms (or bounded morphisms), that is, functional bisimilations introduced in modal logic as basic truth-preserving operations on Kripke frames and models [Goranko and Otto, 2006]. We also observe that, in some cases, these characterizations give rise to rewriting algorithms and complexity bounds for deciding conservative rewritability. The latter results are in sharp contrast to the fact that it is typically undecidable whether a given TBox is a model-conservative rewriting of another TBox [Lutz and Wolter, 2010; Konev et al., 2013]. We focus on standard DLs between ALC and ALCQI, but also briefly consider rewritings into the lightweight DL DL-Litehorn.

Our model-theoretic characterizations are summarized in Table 1, where the criteria for equivalent rewritability are taken from [Lutz, Piro, andWolter, 2011]. Thus, for example, model-conservative ALCI-to-ALC rewritability coincides with subsumption-conservative ALCI-to-ALC-rewritability, and both are characterized by preservation under generated subinterpretations or, equivalently, inverse p-morphisms. In contrast, model-conservative ALCQ-to-ALC rewritability coincides with equivalent ALCQ-to-ALC rewritability, but not with subsumption-conservative ALCQ-to-ALC rewritability. The situation is yet again different for ALCIto-DL-Litehorn rewritability, in which case all three notions coincide. The question marks indicate two cases where characterizations are unknown.

An in-depth exploration of the applicability of our modeltheoretic characterizations is beyond the scope of this paper. We only mention in passing three cases that come naturally along with the preservation criteria. Thus, we show that the preservation conditions for ALCI-to-ALC rewritability are decidable in EXPTIME and give an algorithm constructing polynomial-size rewritings, while those for modelconservative and subsumption-conservative ALCQ-to-ALC rewritabilities give rise to 2EXPTIME decision algorithms.

Related work. Conservative rewritings of TBoxes are ubiquitous in DL research. For example, transformations of TBoxes into normal forms are often model-conservative [Baader, Brandt, and Lutz, 2005; Kazakov, 2009]. We note, however, that some well known DL rewritings introducing fresh symbols that are used as a pre-processing step in reasoning [Ding, Haarslev, and Wu, 2007; Carral et al., 2014b; 2014a] or to prove complexity results for reasoning [De Giacomo, 1995] are not conservative rewritings but only satisfiability preserving. There has been significant work on rewritings of ontology-mediated queries (OMQs), which preserve their certain answers, into datalog or OMQs in weaker DLs [Kaminski and Cuenca Grau, 2013; Bienvenu et al., 2014]. It seems that, from a technical viewpoint, rewritability of OMQs is not related to TBox conservative rewritability. Baader [1996] considers the expressive power of DLs and corresponding notions of rewritability based on a variant of model-conservative extension and discusses the relationship to subsumption-conservative extensions. Another closely related problem is TBox approximation. In this case, rather than aiming at a conservative rewriting, the aim is to compute a TBox in a weaker DL that approximates the consequences of the original TBox [Ren, Pan, and Zhao, 2010; Console et al., 2014].

Detailed proofs can be found in [Konev et al., 2016].

2 Conservative Rewritability

In DLs, concepts and roles are defined inductively starting from countably infinite sets NC of concept names and NR of role names and using a set of constructors. The constructors available in ALCQI are shown in the table below, where the formation of inverse roles is the only role constructor and the remaining four are concept constructors. The third column defines the extensions of roles and concepts with these constructors in an interpretation I = (∆I ↪ ·I ), where ·I maps each concept name A to a subset AI of the domain ∆I of I, and each role name r to rI ✓ ∆I ⇥∆I . In the table, r stands for a role (i.e., a role name or its inverse), A↪B for concept names, and C↪D for (possibly compound) concepts; rI (d) = ¶d0 ♣ (d↪ d0 ) 2 rI ♦ and ♣∆♣ is the cardinality of a set ∆. As usual, we define >, ?, t, ! and $ as standard Boolean abbreviations, 9r▷C (existential restriction) as an abbreviation for (> 1 r C), and 8r▷C (universal restriction) for (6 0 r ≻C). In the sublanguage ALCQ of ALCQI, inverse roles are disallowed; in ALCI, at-least and at-most restrictions are limited to 9r▷C and 8r▷C; and ALC is the common part of ALCQ and ALCI.

at-most restriction (6 n r C) ¶d 2 ∆I ♣ ♣rI (d) \CI ♣  n♦

An L TBox, T , for a DL L is a finite set of concept inclusions (CI) of the form C v D, where C and D are Lconcepts. We write I ♣= C v D if C I ✓ DI and I ♣= T if this holds for all CIs in T , in which case I is said to be a model of T . T is consistent if it has a model. 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 . By sub(T ) we denote the closure under single negation of the set of subconcepts of concepts in T .

Definition 1 An L0 TBox T 0 is an equivalent L0 -rewriting of an L TBox T if T and T 0 have the same models. T is equivalently L0 -rewritable if it has an equivalent L0 -rewriting.

Now we define three notions of TBox rewritability for DLs L and L0 , where L is typically more expressive than L0 .

Equivalent L-to-L0 rewritability was studied by Lutz, Piro, and Wolter [2011], who gave the semantic characterizations in the first column of Table 1. For example, if L is ALCQI, ALCI or ALCQ and L0 is ALC, then an L TBox is equivalently L0 -rewritable iff its class of models is preserved under global bisimulations, which are defined as follows. Given a signature ⌃, a ⌃-bisimulation between interpretations I1 and I2 is a relation S ✓ ∆I1 ⇥∆I2 that satisfies conditions

ALCI-to-DL-Litehorn

[Atom], [Forth] and [Back] in the table below, for r↪A 2 ⌃. In [Back] and elsewhere, 'dual' refers to swapping the rˆoles of I1↪ d1↪ d01 and I2↪ d2↪ d02 . The relation 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. If ⌃ = NC [ NR, we omit ⌃ and say simply '(global) bisimulation.' A TBox T is preserved under global bisimulations if any interpretation that is globally bisimilar to a model of T is a model of T .

Example 1 The ALCI TBox ¶9r-▷B v A♦ can be equivalently rewritten to the ALC TBox ¶B v 8r▷A♦. However, the ALCI TBox T = ¶9r-▷B u 9s-▷B v A♦ is not equivalently ALC-rewritable. Indeed, the interpretation I in the picture below is a model of T and globally bisimilar to the interpretation J , which is not a model of T .

Equivalent ALCQI-to-ALCQ rewritability is characterized by counting bisimulations defined but replacing [Forth] and [Back] in the definition of bisimulations with [QForth] and [QBack]. For equivalent ALCQI-to-ALCI rewritability, we need i-bisimulations, that is, bisimulations for which [Forth] and [Back] hold for inverse roles as well.

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 a signature ⌃, the ⌃- reduct of I is the interpretation I♣⌃ coinciding with I on ⌃ and having XI♣⌃ = ; for 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 called a model-conservative (or m-conservative) extension of T if T 0 ♣= T and, for every I ♣= T , there is I 0 ♣= T 0 such that I =sig(T ) I 0 .

Any equivalent L0 -rewriting of a TBox T is also an mconservative L0 -rewriting of T , but not the other way round:

Definition 2 An L0 TBox T 0 is called an m-conservative L0 - rewriting of an L TBox T if T 0 is an m-conservative extension of T . An L TBox T is m-conservatively L0 -rewritable if it has an m-conservative L0 -rewriting.

Example 2 The ALCI TBox ¶9r-▷B u 9s-▷B v A♦ from Example 1 is m-conservatively ALC-rewritable to

where B9r-▷B, B9s-▷B are fresh concept names.

A TBox T 0 is a subsumption-conservative (s-conservative) extension of an L TBox T if T 0 ♣= T and T 0 ♣= C v D implies T ♣= C v D, for any L-CI C v D given in sig(T ).

Definition 3 An L0 TBox T 0 is an s-conservative L0 - rewriting of an L TBox T if T 0 is an s-conservative extension of T . An L TBox T is s-conservatively L0 -rewritable if it has an s-conservative L0 -rewriting.

Note that it makes sense to speak about an s-conservative L0 -rewriting of a TBox T only if the language of T is understood. For example, the ALC TBox ¶> v 9r▷A u 9r▷≻A♦ is an s-conservative rewriting of T = ¶> v 9r▷>♦ when T is regarded as an ALC TBox, but not as an ALCQ TBox.

Example 3 The ALCQ TBox T = ¶A v ≥ 2 r▷B♦ is sconservatively ALC-rewritable to

Every m-conservatively L0 -rewritable TBox T is s-conservatively L0 -rewritable, but not the converse:

where B1 and B2 are fresh concept names. To show this, note first that T 0 ♣= T . Second, recall that ALCQ TBoxes are complete for ditree interpretations, that is, interpretations I such that rI \ sI = ; for r 6= s and the directed graph with nodes ∆I and edges (d↪ d0 ) 2 Sr2NR rI is a directed tree. Thus, if T 6♣= C v D, for an ALCQ-CI C v D in sig(T ), then there is a ditree model I of T with I 6♣= C v D. Clearly, there exists a model J of T 0 with J =sig(T ) I. But then J 6♣= C v D, and so T 0 6♣= C v D, as required.

However, T 0 is not an m-conservative rewriting of T because (in contrast to ditree models of T ) the model I of T shown below is not the sig(T )-reduct of any model of T 0 .

It is not difficult to generalize this argument to prove that there is no m-conservative ALC-rewriting of T .

Theorem 1 Let L be a DL reflecting disjoint unions, T an L TBox, and let L0 2 ¶ALCQ↪ALCI↪ALC♦. If T is mconservatively (or s-conservatively) L0 -rewritable, then T has a m-conservative (or, respectively, s-conservative) L0 - rewriting not using role names outside sig(T ).

In our examples so far, we used fresh concept names but no fresh role names. This is no accident: for the DLs considered in this paper, fresh role names in conservative rewritings are not required. Say that a DL L reflects 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 a model of T . All of our DLs are known to reflect disjoint unions.

Proof. To illustrate the idea, consider an m-conservative ALC-rewriting T 0 of T . For any C 2 sub(T 0 ) of the form 9r▷C 0 or 8r▷C 0 with r 62 sig(T ), take a fresh concept name BC and denote by D] the result of replacing all top-most occurrences of such C in D 2 sub(T 0 ) by BC. The required m-conservative ALC-rewriting T is given by the inclusions u C2t C ] v ?, where t ranges over maximal subsets of sub(T ) such that u C2t C is not satisfiable with respect to T 0 . Indeed, for any I ♣= T , there is J ♣= T with J =sig(T ) I. To show T ♣= T , suppose I ♣= T and I 6♣= T , with rI = ;

for r 62 sig(T ). By the definition of T , for every d 2 ∆I , there is a ditree model Id of T 0 with root d (and no other shared elements) such that d 2 (C ] )I iff d 2 C Id , for C 2 sub(T 0 ). We remove all (d↪ d0 ) 2 rId with r 2 sig(T ) from Id, d 2 ∆I , and take the union J of the resulting interpretations with I. Then J ♣= T 0 but J 6♣= T (because T reflects disjoint unions and J♣sig(T ) is the disjoint union of the sig(T )-reduct of I and the sig(T )-reducts of Id with d removed), which is a contradiction. o Note that the size of T is exponential in ♣T ♣. It is an interesting open problem whether a polynomial rewriting exists. To see why reflection of disjoint unions is essential, consider the ALCU TBox T = ¶> v 9u▷A♦ with the universal role u, which is a logical symbol and not part of the signature of T [Kr¨otzsch, Simanˇc´ık, and Horrocks, 2012]. Then ¶> v 9r▷A♦ is an m-conservative ALC-rewriting of T but no such rewriting without fresh role names exists.

3 Rewriting Inverse Roles

In this section, we investigate conservative TBox rewritability from DLs with inverse roles to the corresponding DLs without them. First, we give a natural characterization of m- and s-conservative ALC-rewritability of ALCI-TBoxes in terms of generated subinterpretations. Motivated by the observation that preservation under generated subinterpretations does not characterize conservative ALCQI-to-ALCQ rewritability, we then give an alternative characterization of conservative ALCI-to-ALC rewritability in terms of p-morphisms. In contrast to generated subinterpretations, p-morphisms can be lifted to ALCQI, and we show that m- and s-conservative ALCQI-to-ALCQ rewritability is characterized in terms of counting p-morphisms.

An interpretation I is a subinterpretation of J if ∆I ✓ ∆J , AI = AJ \∆I , and rI = rJ \ (∆I ⇥∆I ) for all A and r. I is a generated subinterpretation of J if, in addition, d 2 ∆I and (d↪ d0 ) 2 rJ imply d0 2 ∆I . 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, all ALC TBoxes enjoy this property.

Suppose we want to construct an m-conservative ALCrewriting of an ALCI TBox T . Without loss of generality, we can assume that T uses the concept constructors ≻, u and 9 only. For any role name r in T , take a fresh role name ¯ r. Then, for any 9r▷C in sub(T ), where r is a role (a role name or its inverse), take a fresh concept name B9r▷C. Denote by D] the ALC-concept obtained from any D 2 sub(T ) by replacing every top-most occurrence of a subconcept of the form 9r▷C in D with B9r▷C. Now, let T be an ALC TBox containing C ] v D] , for C v D 2 T , and for r 2 NR,

Clearly, T can be constructed in polynomial time in ♣T ♣.

1. T is m-conservatively ALC-rewritable;

Theorem 2 The following conditions are equivalent for any ALCI TBox T :

1. T is s-conservatively ALC-rewritable;
2. T is preserved under generated subinterpretations;

Proof. We only briefly discuss the proof of (3) ) (4) here. Assume (3). Clearly, for every model I of T , there is a model J of T with J =sig(T ) I. It remains to show that T ♣= T . Suppose I ♣= T . The extension I1 of I in which the interpretation of every ¯ r is extended by the inverse of rI is also a model of T . Let I2 be I1 with every d 2 ∆I1 renamed to d0 . Take the disjoint union J of I1 and I2, and replace each (d↪ e) 2 ¯ rJ such that d↪ e 2 ∆I1 and (e↪ d) ◁2 rJ with (e0 ↪ d) 2 rJ and (d↪ e0 ) 2 ¯ rJ , and add (e0 ↪ d0 ) 2 rJ for any (d0 ↪ e0 ) 2 ¯ rJ with d0 ↪ e0 2 ∆I2 and (e0 ↪ d0 ) ◁2 rJ . Then J ♣= T , with the sig(T )-reduct of I being a generated subinterpretation of the sig(T )-reduct of J . Thus I ♣= T . o

1. T is an m-conservative ALC-rewriting of T .

It is open whether a polynomial-size rewriting without additional role names exists. The proof above shows that to decide whether T is m-conservatively ALC-rewritable, it is enough to check whether T ♣= T , which can be done in EXPTIME [Baader et al., 2003]. A matching EXPTIME lower bound is obtained by reduction of ALCI TBox satisfiability.

Corollary 1 Deciding m-conservative ALCI-to-ALC rewritability is EXPTIME-complete.

The next example shows that preservation under generated subinterpretations does not guarantee conservative ALCQIto-ALCQ rewritability.

The reason why T cannot be conservatively rewritten into an ALCQ TBox is that, without inverse roles, one cannot restrict the number of r-predecessors. To capture this intuition, we introduce a functional version of (counting) bisimulations.

Example 4 Any subinterpretation of a model of the ALCQI TBox T = ¶A v ( 1 r-▷>)♦ is also a model of T , and so T is preserved under generated subinterpretations. We prove below that T is not m-conservatively ALCQ rewritable.

Definition 4 A (counting) ⌃-p-morphism from I1 to I2 is any global (counting) ⌃-bisimulation S between I1 and I2 such that S is a function. If ⌃ = NC [ NR, we refer to S as a (counting) p-morphism. A TBox T is preserved under inverse (counting) p-morphisms if I ♣= T whenever there is a (counting) p-morphism from I to a model of T .

A fundamental property of p-morphisms is established by

Lemma 1 Suppose T is an ALC (or ALCQ) TBox, ⌃ contains all role names in sig(T ), and there is a (counting) ⌃-pmorphism f from an interpretation I to some model I 0 of T . Then there is a model J of T such that J =⌃ I.

Proof. We define J in the same way as I except that we set AJ = f -1 (AI 0 ) for A 2 sig(T ) ∩ ⌃. Then f is a (counting) sig(T )-bisimulation from J to I 0 , and so J ♣= T . o

It follows that if an ALCI (or ALCQI) TBox T is mconservatively ALC- (or ALCQ-) rewritable, then T is preserved under inverse (counting) p-morphisms. Indeed, let f : I1 ! I2 be a p-morphism and T 0 an m-conservative ALC-rewriting of T . By Theorem 1, we may assume that the role names in sig(T 0 ) belong to sig(T ). By Lemma 1, there is a model J1 of T 0 with J1 =sig(T ) I1, from which I1 ♣= T .

Note that if a TBox T reflects disjoint unions and is preserved under inverse p-morphisms, then it is preserved under generated subinterpretations. Indeed, let I be a generated subinterpretation of J ♣= T . Take the disjoint union I 0 = (I⇥¶0♦)[(J ⇥¶1♦) of I and J . The map f : I 0 ! J defined by setting f(d↪ i) = d for i = 0↪ 1 is a p-morphism. Then I 0 ♣= T , and so I ♣= T . Thus, we obtain:

Theorem 3 An ALCI TBox is m-conservatively (and sconservatively) ALC-rewritable iff it is preserved under inverse p-morphisms.

Counting p-morphisms characterize both m- and s-conservative ALCQ-rewritabilities:

1. T is m-conservatively ALCQ-rewritable;

Theorem 4 The following conditions are equivalent for any ALCQI TBox T :

1. T is s-conservatively ALCQ-rewritable;

Proof. We sketch the proof of (3) ) (1) where, unlike Theorem 2, we construct an infinite rewriting T 0 from which a finite one is obtained by compactness. T 0 is defined by brute force: given T , it includes all C ] v D] with T ♣= C v D, where C↪D are ALCQI concepts over sig(T ) and C ] ↪D] are the results of replacing uniformly any top-most qualified number restriction with inverse role by a fresh concept name. The crucial step now is to prove that T 0 ♣= T if T is preserved under inverse counting morphisms. Suppose this is not so. Take an !-saturated model I of T 0 that is not a model of T [Chang and Keisler, 1990, p. 100]. By unraveling I into a tree-shaped interpretation and using preservation under inverse counting p-morphisms, we construct a new I 0 with I 0 ♣= T 0 and I 0 6♣= T , in which no node has more than one r-predecessor (r a role name) satisfying the same ALCQconcepts; cf. Example 5. Now we construct a model J of T containing I 0 as a generated subinterpretation, contrary to T being preserved under inverse counting p-morphisms. o

1. T is preserved under inverse counting p-morphisms.

The decidability of rewritability and the size of rewritings in Theorem 4 remain open.

4 Rewriting Number Restrictions

Now we consider TBox rewritability from DLs with qualified number restrictions to the corresponding DLs without them. We first characterize s-conservative ALCQ-toALC rewritability and ALCQI-to-ALCI rewritability in terms of p-morphisms and, respectively, i-p-morphisms. We then generalize Example 3 and show that m-conservative ALCQ-to-ALC rewritability coincides with equivalent ALCrewritability by characterizing it in terms of preservation under global bisimulations. Finally, we show that this is not the case for m-conservative ALCQI-to-ALCI rewritability.

The next lemma shows that s-conservative ALCQ-to-ALC rewritability can be regarded as a principled approximation of m-conservative rewritability (cf. Example 3).

Lemma 2 An ALC TBox T 0 is an s-conservative rewriting of an ALCQ TBox T iff T 0 is an m-conservative rewriting of T over ditree interpretations of finite outdegree.

Suppose we need an s-conservative ALC-rewriting of an ALCQ-TBox T . As before, we assume that T is built using ≻, u and (> n r C) only. Take fresh concept names BD↪ BD 1 ↪ ▷ ▷ ▷ ↪BD n , for D = (> n r C) 2 sub(T ), and let ⌃ be sig(T ) together with the fresh concept names. For C 2 sub(T ), let C ] be the ALC-concept obtained from C by replacing all top-most occurrences of D = (> n r D0 ) in C with BD. Let T be the infinite TBox containing C ] v D] , for C v D 2 T , and for D = (> n r C) 2 sub(T ),

• BD v 9r▷(C ] uBD 1 ) u · · · u 9r▷(C ] uBD n ),
• BD i v ≻BD j for i 6= j,
• u 1in(9r▷(C ] u C ] i u u j6=i ≻C ] j )) v BD, for any ALCconcepts Ci with sig(Ci) ✓ ⌃.
• T is s-conservatively ALC-rewritable;

Theorem 5 The following conditions are equivalent for any ALCQ TBox T :

1. T is an s-conservative (infinite) ALC-rewriting of T ;

Proof. We sketch (3) ) (2). The interesting step is to prove that T ♣= T . Suppose this is not the case. We find an !- saturated model I of T such that I 6♣= T . Let J be the quotient I◁⇠, where d ⇠ d0 if (d↪ d0 ) is contained in the largest ⌃-bisimulation on I. The map that sends each d 2 ∆I to its equivalence class d◁⇠ in J is a ⌃-p-morphism, and by carefully analysing T one can show that J ♣= T . By (2), I ♣= T , which is a contradiction. o

1. T is preserved under inverse p-morphisms.

Although we do not know how to decide preservation under inverse counting p-morphisms from Theorem 4, preservation under inverse p-morphisms of ALCQ TBoxes can be decided in 2EXPTIME (with numbers coded in unary). The algorithm uses a type elimination argument similar to the one employed for deciding equivalent ALC-rewritability of ALCI TBoxes [Lutz, Piro, and Wolter, 2011]. So we have:

Thus, given an ALCQ TBox T , one can first decide sconservative ALC-rewritability and then, in case of a positive answer, effectively construct a rewriting by going through the finite subsets of T in a systematic way until a finite T 0 ✓ T with T 0 ♣= T is found, which must exist by compactness.

Theorem 6 The problem of s-conservative ALCrewritability of ALCQ TBoxes is decidable in 2EXPTIME.

Our analysis of s-conservative ALC-rewritability of ALCQ TBoxes can be lifted to s-conservative ALCIrewritability of ALCQI TBoxes by replacing (i) ditree interpretations with tree interpretations (in which rI \ sI = ; for all roles r 6= s, and the undirected graph with nodes ∆I and edges ¶d↪ d0 ♦ for (d↪ d0 ) 2 Sr2NR rI is a tree); (ii) pmorphisms with i-p-morphisms (functional i-bisimulations); and (iii) using fresh concept names BD for qualified number restrictions D with inverse roles as well. These modifications give the required generalizations of Lemma 2 and Theorem 5. However, decidability of s-conservative ALCI-rewritability of ALCQI TBoxes remains open.

As to m-conservative ALCQ-to-ALC rewritability, Example 3 shows that the straightforward s-conservative ALCrewriting T 0 of T = ¶A v ≥ 2 r▷B♦ is not an m-conservative rewriting because there is a non-tree interpretation I for which no J ♣= T 0 with J =sig(T ) I exists. A generalization of this argument shows that only ALCQ TBoxes that are preserved under global bisimulations are m-conservatively ALC-rewritable. Thus, we obain:

Theorem 7 An ALCQ TBox is m-conservatively ALCrewritable iff it is equivalently ALC-rewritable.

Using type elimination, one can prove that deciding preservation of ALCQ TBoxes under global bisimulations is in 2EXPTIME. Thus, m-conservative ALC-rewritability of ALCQ TBoxes is decidable in 2EXPTIME.

Surprisingly, the situation is different for m-conservative ALCQI-to-ALCI rewritability, where one would also expect that only equivalently ALCI-rewritable TBoxes (those that are preserved under global i-bisimulations) are mconservatively ALCI-rewritable. However, the following example shows that this is not the case:

Example 6 The TBox T = ¶9r▷> v 9r▷(≥ 2r-▷>)♦ in ALCQI has the m-conservative ALCI-rewriting T 0 = ¶9r▷> v 9r▷(9r-▷B u 9r-▷≻B)♦. No equivalent ALCIrewriting of T exists because it is not preserved under global i-bisimulations. The proof that, for every I ♣= T , there is J ♣= T 0 with J =sig(T ) I relies on the observation that nontree shaped counterexamples such as the one in Example 3 do not exist because of the interaction between T 's constraints for r-successors and r--successors.

We do not have any conjecture as to a natural semantic characterization of m-conservative ALCQI-to-ALCI rewritability. In fact, Theorem 7 and Example 6 together suggest that such a characterization does not exist.

5 ALCQI-to-ALC Rewritability

At first sight, ALCQI-to-ALC rewritability easily reduces to the two-step ALCQI-to-ALCQ-to-ALC rewritability. Note, however, that the first step introduces fresh concept names that are not regarded as auxiliary in the second step. In fact, to smoothly compose the two steps, a more general notion of rewritability with a distinguished set of symbols in the input TBox is needed. Call a TBox T m-conservatively L rewritable relative to a signature ⌃ ✓ sig(T ) if there exists an L-TBox T 0 such that ¶I♣⌃ ♣ I ♣= T ♦ = ¶I♣⌃ ♣ I ♣= T 0 ♦. Investigating this notion is beyond the scope of this paper. We only mention one unexpected result, which can be proved by reduction of the undecidable problem whether an ALC TBox is an m-conservative rewriting of the empty TBox [Konev et al., 2013] (cf. Corollary 1):

Theorem 8 The problem of m-conservative ALCI-to-ALC rewritability relative to a signature ⌃ is undecidable.

As ALC-rewritable ALCQI TBoxes are not preserved under global bisimulations (see Example 2), we cannot simply put together the corresponding characterizations from the previous two sections in order to characterize m-conservative ALC-rewritability of ALCQI TBoxes. Nevertheless, by applying the s-conservative ALCQ rewriting above to the rewriting in the proof of Theorem 4, we obtain an s-conservative ALC-rewriting of an input ALCQI TBox T iff T is preserved under inverse p-morphisms iff such a rewriting exists at all.

Theorem 9 An ALCQI TBox is s-conservatively ALCrewritable iff it is preserved under inverse p-morphisms.

For m-conservative rewritability, we have:

Theorem 10 If an ALCQI TBox is preserved under global i-bisimulations and inverse p-morphisms, then it is m-conservatively ALC-rewritable.

Proof. From preservation under global i-bisimulations of T follows the existence of an equivalent ALCI TBox T 0 . Then T is m-conservatively ALC-rewritable iff T 0 is mconservatively ALC-rewritable iff T 0 is preserved under inverse p-morphisms (Theorem 3). o

We conjecture that the converse also holds. By Lemma 1, m-conservatively ALC-rewritable ALCQI TBoxes are preserved under inverse p-morphims. Thus, the conjecture would follow from preservation under global i-bisimulations.

6 Discussion and FutureWork

Up to now, our focus has been on rewritability between expressive DLs. However, rewritability to the lightweight DLs from the DL-Lite and EL families is of great interest as well. Table 1 gives our model-theoretic characterization of rewritability from ALCI to DL-Litehorn (without role inclusions) [Calvanese et al., 2007; Artale et al., 2009]. The characterization of equivalent rewritability in terms of products and succ-simulations was given by Lutz, Piro, and Wolter [2011]. It is straightforward to prove that it also applies to m- and s-conservative rewritability of ALCI TBoxes by first showing that Theorem 1 holds for rewritings into DL-Litehorn as well:

Theorem 11 For ALCI TBoxes, equivalent DL-Litehornrewritability, m-conservative DL-Litehorn-rewritability, as well as s-conservative DL-Litehorn-rewritability coincide and are EXPTIME-complete.

Rewritability into DL-Lite dialects with role inclusions (where Theorem 1 does not hold) and into EL appear to be much more challenging and a detailed study remains for future work. More generally, at the moment we only fully understand conservative ALCI-to-ALC-rewritability; in all other cases, it remains to determine the optimal size of rewritings, the complexity of computing them, as well as tight bounds for the complexity of deciding rewritability. Based on the resulting algorithms, it would be of great interest to study conservative rewritability in practice and, in particular, determine the rewritability status of real-world ontologies.

Acknowledgments. This work has been supported by EPSRC UK grants EP/M012646/1 and EP/M012670/1 (iTract), and ERC grant 647289 (CODA).