# conservative_rewritability_of_description_logic_tboxes__d01e1e46.pdf

Conservative Rewritability of Description Logic TBoxes

Boris Konev,1 Carsten Lutz,2 Frank Wolter1 and Michael Zakharyaschev3

1Univ. of Liverpool, UK 2Univ. of Bremen, Germany 3Birkbeck, Univ. of London, UK {konev,wolter}@liverpool.ac.uk clu@informatik.uni-bremen.de michael@dcs.bbk.ac.uk

We investigate the problem of conservative rewritability of a TBox T in a description logic (DL) L into a TBox T 0 in a weaker DL L0. We focus on model-conservative rewritability (T 0 entails T and all models of T are expandable to models of T 0), subsumption-conservative rewritability (T 0 entails T and all subsumptions in the signature of T entailed by T 0 are entailed by T ), and standard DLs between ALC and ALCQI. We give model-theoretic characterizations of conservative rewritability via bisimulations, inverse p-morphisms and generated subinterpretations, and use them to obtain a few rewriting algorithms and complexity results for deciding rewritability.

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, modeland 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, and Wolter, 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 rewritabil-

Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI-16)

Rewritability Equivalent Model Conservative Subsumption Conservative ALCI-to-ALC global bisimulations generated subinterpretations/p-morphisms 1

ALCQI-to-ALCQ global counting bisimulations counting p-morphisms 1

ALCQ-to-ALC global bisimulations p-morphisms 1

ALCQI-to-ALCI global i-bisimulations ? i-p-morphisms 1

ALCQI-to-ALC global bisimulations ? p-morphisms 1

ALCI-to-DL-Litehorn products and succ-simulations

Table 1: Model-theoretic characterizations of rewritability.

ity 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 r I 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; r I(d) = {d0 | (d, d0) 2 r I} 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.

constructor syntax semantics

inverse role r (r I) 1 = {(d, e) | (e, d) 2 r I}

negation C I \ CI

conjunction C u D CI \ DI

at-least restriction (> n r C) {d 2 I | |r I(d) \ CI| n}

at-most restriction (6 n r C) {d 2 I | |r I(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 CI 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 .

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

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.

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

[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, d0

1 and I2, d2, d0

2. 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 .

[Atom] for all (d1, d2) 2 S, d1 2 AI1 iff d2 2 AI2

[Forth] if (d1, d2) 2 S and d0

1 2 r I1(d1), r 2 NR, then there is a d0

2 2 r I2(d2) with (d0

2) 2 S. [Back] dual of [Forth] [QForth] if (d1, d2) 2 S and D1 r I1(d1) is finite, r 2 NR, then there is a D2 r I2(d2) such that S contains a bijection between D1 and D2. [QBack] dual of [QForth]

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 I0 |= T 0 such that I =sig(T ) I0.

Definition 2 An L0 TBox T 0 is called an m-conservative L0rewriting 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.

Any equivalent L0-rewriting of a TBox T is also an mconservative L0-rewriting of T , but not the other way round: Example 2 The ALCI TBox {9r .B u 9s .B v A} from Example 1 is m-conservatively ALC-rewritable to

{B v 8r.B9r .B, B v 8s.B9s .B, B9r .B u B9s .B v A},

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 L0rewriting 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.

Every m-conservatively L0-rewritable TBox T is s-conservatively L0-rewritable, but not the converse: Example 3 The ALCQ TBox T = {A v 2 r.B} is sconservatively ALC-rewritable to

T 0 = {A v 9r.B1, A v 9r.B2, B1 v B2, B1t B2 v B},

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 r I \ s I = ; for r 6= s and the directed graph with nodes I and edges (d, d0) 2 S

r2NR r I 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.

B B B r r r r

It is not difficult to generalize this argument to prove that there is no m-conservative ALC-rewriting of 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 S

i2I 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. 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) L0rewriting not using role names outside sig(T ). 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.C0 or 8r.C0 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 r I = ; 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 CId, for C 2 sub(T 0). We remove all (d, d0) 2 r Id 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 mand 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 mand 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 r I = r J \ ( I I) for all A and r. I is a generated subinterpretation of J if, in addition, d 2 I and (d, d0) 2 r J 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,

C] v 8 r.B9r.C, B9r.C 9r.C], for 9r.C 2 sub(T ),

C] v 8r.B9r .C, B9r .C 9 r.C], for 9r .C 2 sub(T ).

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

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

(1) T is m-conservatively ALC-rewritable; (2) T is s-conservatively ALC-rewritable;

(3) T is preserved under generated subinterpretations; (4) T is an m-conservative ALC-rewriting of T .

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 r I 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 r J such that d, e 2 I1 and (e, d) /2 r J with (e0, d) 2 r J and (d, e0) 2 r J , and add (e0, d0) 2 r J for any (d0, e0) 2 r J with d0, e0 2 I2 and (e0, d0) /2 r J . 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

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.

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.

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.

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 I0 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(AI0) for A 2 sig(T ) \ . Then f is a (counting) sig(T )-bisimulation from J to I0, 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 .

Example 5 The map f : I1 ! I2 below is a counting pmorphism. Since I2 is a model of T from Example 4 but I1 is not, T is not m-conservatively ALCQ-rewritable.

A r I2 I1 f

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 I0 = (I {0})[(J {1}) of I and J . The map f : I0 ! J defined by setting f(d, i) = d for i = 0, 1 is a p-morphism. Then I0 |= 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 mand s-conservative ALCQ-rewritabilities: Theorem 4 The following conditions are equivalent for any ALCQI TBox T :

(1) T is m-conservatively ALCQ-rewritable; (2) T is s-conservatively ALCQ-rewritable; (3) T is preserved under inverse counting p-morphisms. 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 I0 with I0 |= T 0 and I0 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 I0 as a generated subinterpretation, contrary to T being preserved under inverse counting p-morphisms. o

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-to ALC 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 ),

j for i 6= j,

BD v 9r.(C] u BD

1 ) u u 9r.(C] u BD

u 1 i n(9r.(C] u C]

j)) v BD, for any ALC-

concepts Ci with sig(Ci) .

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

(1) T is s-conservatively ALC-rewritable; (2) T is an s-conservative (infinite) ALC-rewriting of T ; (3) T is preserved under inverse p-morphisms.

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

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: Theorem 6 The problem of s-conservative ALCrewritability of ALCQ TBoxes is decidable in 2EXPTIME.

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.

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 r I \ s I = ; for all roles r 6= s, and the undirected graph with nodes I and edges {d, d0} for (d, d0) 2 S

r2NR r I 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 Future Work 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 mand 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 (i Tract), and ERC grant 647289 (CODA).

[Artale et al., 2009] Artale, A.; Calvanese, D.; Kontchakov,

R.; and Zakharyaschev, M. 2009. The DL-Lite family and relations. Journal of Artificial Intelligence Research 36:1 69.

[Baader et al., 2003] Baader, F.; Calvanese, D.; Mc Guin-

ness, D. L.; Nardi, D.; and Patel-Schneider, P. F., eds. 2003. The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press.

[Baader, Brandt, and Lutz, 2005] Baader, F.; Brandt, S.; and

Lutz, C. 2005. Pushing the EL Envelope. In Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, Edinburgh, Scotland, UK, July 30-August 5, 2005, 364 369.

[Baader, 1996] Baader, F. 1996. A formal definition for the

expressive power of terminological knowledge representation languages. J. Log. Comput. 6(1):33 54.

[Bienvenu et al., 2014] Bienvenu, M.; ten Cate, B.; Lutz, C.;

and Wolter, F. 2014. Ontology-based data access: A study through disjunctive datalog, CSP, and MMSNP. ACM Trans. Database Syst. 39(4):33.

[Calvanese et al., 2007] Calvanese, D.; De Giacomo, G.;

Lembo, D.; Lenzerini, M.; and Rosati, R. 2007. Tractable reasoning and efficient query answering in description logics: The DL-Lite family. J. Autom. Reasoning. 39(3):385 429.

[Carral et al., 2014a] Carral, D.; Feier, C.; Grau, B. C.; Hit-

zler, P.; and Horrocks, I. 2014a. EL-ifying ontologies. In Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings, 464 479.

[Carral et al., 2014b] Carral, D.; Feier, C.; Romero, A. A.;

Grau, B. C.; Hitzler, P.; and Horrocks, I. 2014b. Is your ontology as hard as you think? Rewriting ontologies into simpler DLs. In Informal Proceedings of the 27th International Workshop on Description Logics, Vienna, Austria, July 17-20, 2014., 128 140.

[Chang and Keisler, 1990] Chang, C., and Keisler, H. 1990.

Model Theory. North-Holland, Amsterdam.

[Console et al., 2014] Console, M.; Mora, J.; Rosati, R.;

Santarelli, V.; and Savo, D. F. 2014. Effective computation of maximal sound approximations of description logic ontologies. In The Semantic Web - ISWC 2014 - 13th International Semantic Web Conference, Riva del Garda, Italy, October 19-23, 2014. Proceedings, Part II, 164 179.

[De Giacomo, 1995] De Giacomo, G. 1995. Decidability of Class-Based Knowledge Representation Formalisms. Ph.D. Dissertation, Universit a di Roma.

[Ding, Haarslev, and Wu, 2007] Ding, Y.; Haarslev, V.; and

Wu, J. 2007. A new mapping from ALCI to ALC. In Proceedings of the 2007 International Workshop on Description Logics, Brixen-Bressanone, Italy, 8-10 June, 2007.

[Ghilardi, Lutz, and Wolter, 2006] Ghilardi, S.; Lutz, C.; and Wolter, F. 2006. Did I damage my ontology? A case for conservative extensions in description logics. In Proceedings, Tenth International Conference on Principles of Knowledge Representation and Reasoning, Lake District of the United Kingdom, June 2-5, 2006, 187 197. [Goranko and Otto, 2006] Goranko, V., and Otto, M. 2006.

Model Theory of Modal Logic. Handbook of Modal Logic, 255 325. Elsevier. [Kaminski and Cuenca Grau, 2013] Kaminski, M., and Cuenca Grau, B. 2013. Sufficient conditions for firstorder and datalog rewritability in ELU. In Proceedings of the 26th International Workshop on Description Logics, Ulm, Germany, July 23 - 26, 2013, 271 293. [Kazakov, 2009] Kazakov, Y. 2009. Consequence-driven reasoning for Horn SHIQ ontologies. In IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, July 11-17, 2009, 2040 2045. [Konev et al., 2009] Konev, B.; Lutz, C.; Walther, D.; and

Wolter, F. 2009. Formal properties of modularisation. In Modular Ontologies: Concepts, Theories and Techniques for Knowledge Modularization. 25 66. [Konev et al., 2013] Konev, B.; Lutz, C.; Walther, D.; and

Wolter, F. 2013. Model-theoretic inseparability and modularity of description logic ontologies. Artif. Intell. 203:66 103. [Konev et al., 2016] Konev, B.; Lutz, C.; Wolter, F.; and Za-

kharyaschev, M. 2016. Conservative Rewritability of Description Logic TBoxes. Technical report (cgi.csc.liv.ac. uk/ frank/publ/publ.html). [Kr otzsch, Simanˇc ık, and Horrocks, 2012] Kr otzsch, M.; Simanˇc ık, F.; and Horrocks, I. 2012. A description logic primer. Co RR abs/1201.4089. [Lutz and Wolter, 2010] Lutz, C., and Wolter, F. 2010. De-

ciding inseparability and conservative extensions in the description logic EL. J. Symb. Comput. 194 228. [Lutz, Piro, and Wolter, 2011] Lutz, C.; Piro, R.; and Wolter,

F. 2011. Description logic TBoxes: Model-theoretic characterizations and rewritability. In Proceedings of the 22nd International Joint Conference on Artificial Intelligence, Barcelona, Catalonia, Spain, July 16-22, 2011, 983 988. [Ren, Pan, and Zhao, 2010] Ren, Y.; Pan, J. Z.; and Zhao, Y.

2010. Soundness preserving approximation for TBox reasoning. In Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2010, Atlanta, Georgia, USA, July 11-15, 2010.