Conservative Extensions in Expressive Description Logics

1 Introduction

The design and integration of ontologies formulated in modern ontology languages such as OWL is a serious challenge. Experience shows that principled methodologies as well as automated reasoning support are required to ensure that the resulting ontologies are well-structured [6]. In the recent papers [4; 5; 3; 1], conservative extensions have been identified as a crucial notion for formalizing central tasks in ontology design and integration. Consequently, conservative extensions can play a key role in design and integration methodologies [3], and reasoning about conservative extensions can provide valuable support for the ontology designer.

Formally, an ontology T1 ∪ T2 is a conservative extension of an ontology T1 w.r.t. a signature Γ iff every consequence of T1 ∪ T2 formulated in Γ is already a consequence of T1. For example, assume that ontologies are formalized in a description logic (DL) such as OWL-DL and its fragments [2]. Then a signature is a set of concept and role names, an ontology is a DL TBox, and a consequence of a TBox is a subsumption relationship between two concepts which follows from the TBox. Intuitively, T1 ∪ T2 is a conservative extension of T1 w.r.t. Γ if adding T2 to T1 does not change the ontology T1 as far as concepts built only from concept and role names in Γ are concerned. We give three examples of ontology related tasks that can be understood in terms of conservative extensions.

• Ontology refinement. During ontology design, a frequent task is to add more details to a part of the ontology that has not yet been sufficiently described. Intuitively, such a refinement should have no impact on other, unrelated parts of the ontology. This requirement can be formalized by demanding that the refined ontology is a conservative extension of the original one w.r.t. the concept and role names that do not belong to the refined part [4; 1].
• Ontology merging. The most straightforward way to integrate two ontologies is to simply take their union. Such a merging should not compromise the original ontologies. One possible formalization of this requirement is to demand that the united ontology is a conservative extension of the component ontologies w.r.t. the set of all concept and role names used in the respective components. Weaker formalizations are obtained by excluding from the signature concept and role names for which an interaction between the component ontologies is expected (and intended) [4].
• Defining Modules. A module inside an ontology T that describes an independent part of the application domain can be defined as a subset T ′ of T such that T is a conservative extension of T ′ w.r.t. the concept names and role names that belong to T ′ [5].

The most basic reasoning task regarding conservative extensions is as follows: given ontologies T1 and T2 and a signature Γ, decide whether T1 ∪ T2 is a conservative extension of T1 w.r.t. Γ. In the following, we refer to this task as deciding conservative extensions. In [4], this decision problem is investigated for the basic DL ALC and proved to be 2EXPTIMEcomplete. The aim of the current paper is to investigate conservative extensions in more expressive DLs such as the ones underlying the ontology language OWL-DL and to map out the boundary between decidable and undecidable. Our main results are as follows: (i) in ALCQI, the extension of ALC with inverse roles and qualifying number restrictions, deciding conservative extensions is 2-EXPTIME complete and thus not more difficult than in ALC; and (ii) if we further extend ALCQI with nominals, conservative extensions in the resulting DL ALCQIO are undecidable. This shows that conservative extensions in OWL-DL, of which ALCQIO is a fragment, is also undecidable. It also identifies ALCQI as a significant fragment of OWL-DL in which conservative extensions are still decidable.

In mathematical logic, there exist (at least) two versions of conservative extensions. One is based on the consequence relation as sketched above. An alternative, stronger version is defined in a model-theoretic way. We also consider deciding the latter kind of conservative extensions and show that, already in ALC, this problem is highly undecidable. Details of all proofs can be found in the technical report [8].

2 Preliminaries

In DLs, concepts are inductively defined with the help of a set of constructors, starting with a set NC of concept names, a set NR of role names, and (possibly) a set NI of individual names. In this paper, we consider the DL ALCQIO and its fragments. The constructors available in ALCQIO are shown in Figure 1. There, the inverse constructor is the only role constructor, whereas the remaining constructors are concept constructors. In Figure 1 and the remainder of this paper, we use #S to denote the cardinality of a set S, a and b to denote individual names, r and s to denote roles (i.e., role names and inverses thereof), A,B to denote concept names, and C,D to denote (possibly complex) concepts. For an inverse role s = r- we set s:= r. As usual, we use ⊤ as abbreviation for an arbitrary (but fixed) propositional tautology, ⊥ for ¬⊤, ⊔, →, and ↔ for the usual Boolean abbreviations, (⩾ n r C) (at-least restriction) for ¬(⩽ n - 1 r C) if n > 0 and for ⊤ if n = 0 , (= n r C) for (⩽ n r C) ⊓ (⩾ n r C), ∃r.C (existential restriction) for (⩾ 1 r C), and ∀r.C (universal restriction) for (⩽ 0 r ¬C). We assume that the numbers inside number restrictions are coded in binary.

The DL that allows only for negation, conjunction, disjunction, and universal and existential restrictions is called ALC. The availability of additional constructors is indicated by concatenation of a corresponding letter: Q stands for number restrictions; I stands for inverse roles, and O for nominals. This explains the name ALCQIO, and also allows us to refer to its sublanguages in a simple way.

The formulation of ontologies in description logics is based on TBoxes, and we will from now on use these two terms interchangeably. Formally, a TBox is a finite set of concept implications C ⊑ D.

The semantics of ALCQIO-concepts is defined in terms of an interpretation I = (ΔI , ·I ). The domain ΔI is a nonempty set of individuals and the interpretation function ·I maps each concept name A ∈ NC to a subset AI of ΔI , each role name r ∈ NR to a binary relation rI on ΔI , and each individual name a ∈ NI to an individual aI ∈ ΔI . The extension of ·I to inverse roles and arbitrary concepts is defined inductively as shown in the third column of Figure 1.

An interpretation I satisfies an implication C ⊑ D if CI ⊆ DI , and I is a model of a TBox T if it satisfies all implications in T . A concept C is satisfiable relative to a TBox T if there exists a model I of T such that CI ̸= ∅. A concept C is subsumed by a concept D relative to a TBox T (written T |= C ⊑ D) if every model I of T satisfies the implication C ⊑ D.

Despite the fact that individual names are closer to constants than to predicates, we henceforth use the term predicates to refer to elements of NC ∪ NR ∪ NI. A signature is a finite set of predicates. The signature sig(T ) of a TBox T is the set of all predicates that occur in T . Given a description logic L and a signature Γ, we use L(Γ) to denote the set of L-concepts that use only predicates from Γ.

Definition 1 (Conservative Extension) Let T1 and T2 be TBoxes formulated in a DL L, and let Γ ⊆ sig(T1) be a signature. Then T1 ∪ T2 is a Γ-conservative extension of T1 if for all C1, C2 ∈ L(Γ), we have T1 |= C1 ⊑ C2 iff T1 ∪ T2 |= C1 ⊑ C2.

Deciding conservative extensions means to decide, given two TBoxes T1 and T2 and a signature Γ ⊆ sig(T1), whether T1 ∪ T2 is a Γ-conservative extension of T1.

If Γ = sig(T1), we simply drop Γ and only talk about conservative extensions. It is not difficult to see that an alternative definition of conservative extensions is as follows: T1 ∪ T2 is a Γ-conservative extension of T1 iff each concept C ∈ L(Γ) that is satisfiable relative to T1 is satisfiable relative to T1∪T2. Therefore, a concept C ∈ L(Γ) that is satisfiable relative to T1, but not relative to T1 ∪ T2 witnesses that T1 ∪ T2 is not a conservative extension of T1. We call such a concept a witness concept.

Let us give an example for conservative extensions in the description logic ALCQI. Assume that T1 is a TBox formalizing knowledge about universities:

Lecture ⊑ ∃has subject.Subject ⊓ ∃given by.Lecturer

Intro TCS ⊑ Lecture Lecturer ⊑ Professor ⊔TeachingAssistant Lecturer ⊑ ∃employed by.University University ⊑ ∀employed by-.(Academic ⊔Admin)

The upper part of T1 describes university lectures, saying, e.g., that every introductory lecture on theoretical computer science (TCS) is a lecture. The lower part of T1 describes universities and their employees. Suppose now that we want to refine the part of the ontology that is concerned with lectures. We extend the signature by adding the concept names AutomataTheory and ComplexityTheory and state in T2 that these subjects are discussed in every introductory TCS lecture. We also say that automata theory and complexity theory are different things:

Intro TCS ⊑ ∃has subject.AutomataTheory Intro TCS ⊑ ∃has subject.ComplexityTheory ⊥ ⊒ AutomataTheory ⊓ComplexityTheory

Intuitively, this addition should have an impact on the upper part of T1 since it adds information about lectures, but it should not affect the lower part which is not concerned with lectures. This intuition can be formally captured by conservative extensions: if we choose Γ to be the set of all predicates used in the lower part of T1, then T1 ∪ T2 is a Γ-conservative extension of T1. Thus, the lower part of T1 is not affected by the addition of T2. If we choose Γ to be the predicates in the upper part of T1, then T1 ∪ T2 is not a Γ-conservative extension, a witness concept being

By considering these two cases of conservative extensions, the ontology designer can thus verify that his modification changes the TBox (only) in the intended way.

This example also shows that conservative extensions depend on the descripion logic L: the TBoxes T1 and T2 are actually formulated in ALCI and we have seen that if Γ is the set of predicates in the upper part of T1, then T1 ∪ T2 is not a Γ-conservative extension of T1. However, this only holds since we assumed ALCQI to be the underlying DL and thus allowed number restrictions in the witness concept. If we switch the underlying DL to ALCI, then T1 ∪ T2 is a Γ-conservative extension of T1, for the same Γ. In the next section, we investigate a purely model-theoretic version of convervative extension, which does not depend on the language.

2.1 Model Conservative Extensions

In mathematical logic and software specification [9], there are two different kinds of conservative extensions: one that is based on the consequence relation "|=" as in Definition 1 and one that is based on models only . For simplicity, we formulate this second notion only for the case where Γ = sig(T1).

Definition 2 (Model Conservative Extension) Let T1 and T2 be TBoxes. We say that T1 ∪ T2 is a model conservative extension of T1 iff for every model I of T1, there exists a model of T1 ∪ T2 which can be obtained from I by modifying the interpretation of the predicates in sig(T2) \ sig(T1) while leaving the predicates in sig(T1) fixed.

To distinguish the two versions of conservative extensions, in this section we call the one based on "|=" a deductive conservative extension.

The notion of a model conservative extension is more strict than the deductive one: if T1 ∪ T2 is a model conservative extension of T1, then it is clearly also a deductive conservative extension of T1, but the converse does not hold. To see the latter, consider the TBoxes

It is not hard to see that T1 ∪ T2 is a deductive conservative extension of T1 if ALC (or even ALCQI) is the language for witness concepts, but it is not a model conservative extension. The stronger notion of model conservative extensions is of interest for query answering modulo ontologies. In this case, one might want to ensure that under the addition of any ABox A (over the signature of T1) the answers to queries (over the signature of T1) to T1 ∪T2 ∪A coincide with those to T1 ∪A. This immedialy follows if T1 ∪ T2 is a model conservative extension of T1, but it does not follow if T1 ∪ T2 is just a deductive conservative extension of T1.

However, from an algorithmic viewpoint model conservative extensions are a problematic choice: we show that they are highly undecidable even in the basic description logic ALC (and therefore also in all its extensions). The proof of the following result is by a reduction from the semantic consequence problem in modal logic and can be found in [8].

Theorem 3 It is Π11 -hard to decide whether for two given ALC TBoxes T1 and T2, the TBox T1 ∪ T2 is a model conservative extension of T1.

3 Decidability in ALCQI

We give a tight complexity bound for deciding conservative extensions in ALCQI. We use |C| to denote the length of a concept C, and |T | to denote the size ∑C⊑D∈T (|C| + |D|) of a TBox T .

Theorem 4 It is 2-EXPTIME-complete to decide conservative extensions in ALCQI. In the case that T1 ∪ T2 is not a conservative extension of T1, there exists a witness concept C of length at most 3-exponential in |T1 ∪ T2| that can be computed in time polynomial in |C|.

The lower bound can be proved exactly in the same way as the 2-EXPTIME lower bound for conservative extensions in ALC [4]. However, the lower bounds fromALC do not simply transfer to ALCQI and it is necessary to walk through the proof in [4] and check that it also works for the case of ALCQI. In the following, we concentrate on proving the upper bound. It is established by devising a 2-EXPTIME algorithm that, for convenience, decides non-conservative extensions.

We start by reminding that ALCQI has the tree model property. More precisely, a tree interpretation is an interpretation I = (ΔI , ·I ,<I ) equipped with an additional relation <I ⊆ ΔI × ΔI such that (i) (ΔI ,<I ) is a tree, (ii) ⋃r∈NR rI ∪ r-I = < ∪ <-1 , and (iii) sI and rI are disjoint for all distinct roles s and r. In ALCQI, every concept C that is satisfiable relative to a TBox T is satisfiable in a tree model of T , i.e., a model of T that is a tree interpretation [7]. In this section, when talking of an interpretation or model of a TBox we always mean a tree interpretation.

To develop the algorithm for deciding non-conservative extensions in ALCQI, we introduce a new kind of witness for non-conservativity. The new witnesses are very similar to finite tree interpretations and easier to work with than witness concepts. For a signature Γ, let a literal type S for Γ be a subset of lit(Γ) := {A, ¬A | A ∈ Γ ∩ NC} such that for each A ∈ Γ ∩ NC, A ∈ S iff ¬A /∈ S. A Γ-role is a role r such that r or r- is in Γ.

Definition 5 (Γ-tree) A Γ-tree T = (W,<,L,O) is a finite intransitive tree (W,<) such that each node w ∈ W is labeled by a literal type L(w) for Γ, each edge (w,w′ ) is labeled by a Γ-role L(w,w′ ), and O ⊆ W is a set of leafs of (W, <).

Essentially, a Γ-tree is a finite tree interpretation equipped with an additional unary predicate O denoting a subset of the leafs. The following definition provides a way to relate Γtrees and actual interpretations.

Definition 6 (Γ-embedding) Let T = (W, <, L, O) be a Γtree with root w ∈ W, and I an interpretation with root d ∈ ΔI . A Γ-embedding f : T → I is an injection from W to ΔI such that

• f(w) = d,
• L(v, v′ ) = r iff f(v)rI f(v′ ), for all v, v′ ∈ W and Γroles r,
• C ∈ L(v) iff f(v) ∈ CI , for all v ∈ W and C ∈ lit(Γ),
• if v ̸∈ O, then every d′ ∈ ΔI with f(v)rI d′ for some Γ-role r is in the range of f.

T is called Γ-embeddable into I if there is a Γ-embedding f : T→ I.

The definition illustrates that Γ-trees represent a (finite) initial part of (potentially infinite) tree interpretations. This explains the predicate O of Γ-trees: O marks those leafs in the Γ-tree that are not necessarily leafs in the tree interpretation I that we embed into. We can now establish Γ-trees as witnesses for non-conservativity.

Lemma 7 T1 ∪ T2 is not a conservative extension of T1 w.r.t. Γ iff there exists a Γ-tree T = (W,<,L,O) which is Γembeddable into a model of T1 but not into any model of T1 ∪ T2.

The general idea behind the algorithm is as follows: by Lemma 7, to decide whether T1 ∪ T2 is not a conservative extension of T1, it suffices to decide whether there exists a Γtree that is Γ-embeddable into a model of T1, but not into any model of T1∪T2. This is what our algorithmwill do. Alas, we conjecture that there are cases in which the smallest such tree is 3-exponential in |T1 ∪ T2|, and therefore a 2-exponential algorithm cannot simply try to construct such a tree. Instead, we check the existence of the Γ-tree by searching for certain witnesses for the existence of such a tree. Before we can introduce these witnesses (which should not be confused with Γ-trees as witnesses for non-conservativity), we need to introduce the notion of a type.

Definition 8 (Type) Let T be a TBox. We use cl(T ) to denote the smallest set that contains all concepts in T and is closed under single negations and under subconcepts. A T - type t is a subset of cl(T ) such that

• ¬C ∈ t iff C ̸∈ t, for all ¬C ∈ cl(T );
• C1 ⊓ C2 ∈ t iff C1 ∈ t and C2 ∈ t, for all C1 ⊓ C2 ∈ cl(T ).

Given an interpretation I and u ∈ ΔI , the set

is a T -type. In what follows, we will not always distinguish between the type t and the conjunction of all members of t. We now introduce a witness for the existence of a Γ-tree that is Γ-embeddable into a model of T1, but not into any model of T1 ∪ T2. To avoid writing sub- and superscripts, from now on we assume the input T1, T2, and Γ to be fixed.

Definition 9 (Root pair, Internal pair) A root pair (t,U) consists of a T1-type t and a set U of T1 ∪ T2-types. An internal pair (t′ →r t,U) consists of a Γ-role r, T1-types t′ and t, and a function U mapping each T1 ∪ T2-type to a set of T1 ∪ T2-types.

Intuitively, each (root or internal) pair encodes relevant information about possible embeddings of a Γ-tree into models of T1 and T1 ∪ T2. This is made precise by the notion of realizability.

Definition 10 (Realizable root pair) Let T = (W, <, L, O) be a Γ-tree. A root pair (t, U) is realized by T iff

1. there exist a model I of T1 with root d ∈ tI and a Γembedding f : T→ I;
2. for every T1 ∪ T2-type s, we have s ∈ U iff there exist a model I of T1 ∪ T2 with root d ∈ sI and a Γ-embedding f : T→ I.

While root pairs encode information about possible embeddings of a Γ-tree into models of T1 and T1 ∪T2, internal pairs encode information about possible embeddings of a Γ-tree into rooted submodels of models of T1 and T1 ∪ T2. In the following, if I is a (tree) interpretation and d ∈ ΔI , we write Id to denote the sub-tree interpretation of I rooted at d.

Definition 11 (Realizable internal pair) Let T = (W,<,L,O) be a Γ-tree. An internal pair (t′ →r t,U) is realized by T iff

• there exist a model I of T1 and d′ , d ∈ ΔI such that d′ ∈ (t′ )I , d′ rI d, d ∈ tI , and there is a Γ-embedding f : T→ Id;
• for all T1 ∪ T2-types s, s′ , we have s′ ∈ U(s) iff there exist a model I of T1 ∪ T2 and d′ , d ∈ ΔI such that d′ ∈ (s′ )I , d′ rI d, d ∈ sI , and there is a Γ-embedding f : T→ Id.

A (root or internal) pair is realizable if there exists a Γ-tree T which realizes it.

Observe that internal pairs store information not only about the element d ∈ ΔI to which the root of T is mapped, but also comprise the type t′ of the predecessor d′ of d in I and the (unique!) role r which connects d′ and d. This is necessary due to the presence of inverse roles and number restrictions and bears some similarity to the double blocking technique in tableau algorithms; see [7]. Also note that the U-component of internal pairs is a function rather than a set because, intuitively, the possible types of d in models of T1 ∪ T2 depend on the type of the predecessor d′ in such models.

Let us now describe the algorithm. By Lemma 7 and definition of realizability, there exists a realizable root pair of the form (t, ∅) iff T1 ∪ T2 is not a conservative extension of T1 w.r.t. Γ. The algorithm for deciding non-conservative extensions searches for such a root pair. The easiest case is that a root pair (t, ∅) is realized by a singleton Γ-tree, i.e., a Γ-tree that consists of only a single node. This special case is tested first. If the test is not successful, we must check whether there is a root pair (t, ∅) that is realized by a non-singleton tree T = (W,<,L,O). Assume that this is the case and that the root of T is w. Then each subtree of T rooted at a succesor node w′ of w realizes an internal pair (ˆ t′ →ˆ r ˆ t, ˆU) with ˆ t′ = t and ˆ r = L(w,w′ ). Intuitively, this means that we can check realization of the root pair (t, ∅) in T based on the realization of internal pairs in trees of strictly smaller height. Similarly, we can check the realizability of internal pairs in a Γ-tree based on the realizability of internal pairs in Γ-trees of strictly smaller height. Based on these observations, our algorithm repeatedly generates internal pairs that are realized by Γ-trees of larger and larger height until all such pairs are generated. It then checks whether there exists a root pair (t, ∅) that is realizable based on the generated internal pairs. The following definition formalizes one step of the algorithm in which root pairs or new internal pairs are generated from an existing set of internal pairs.

In the following, if T is a Γ-tree and w ∈ W, we write Tw to denote the sub-tree of T rooted at w.

Definition 12 (One step) Let R be a set of internal pairs. A root pair (t,U) (resp. internal pair (t′ →r t,U)) can be obtained in one step from R if there exists a Γ-tree T = (W, <, L, O) with root w such that

• T realizes (t,U) (resp. (t′ →r t,U));
• for all w′ ∈ W with w < w′ , there exists an internal pair p = (ˆ t′ →ˆ r ˆ t, ˆU) ∈ R such that ˆ t′ = t, ˆ r = L(w, w′ ), and p is realized by Tw′ .

The details of our algorithm are given in Figure 2, where

Intuitively, considering only a subset of Ri of cardinality mT1,T2 means that we limit our attention to Γ-trees of outdegree mT1,T2 . This is justified by the following lemma.

Lemma 13 If T1 ∪ T2 is not a conservative extension of T1 w.r.t. Γ, then there exists a root pair (t, ∅) realized by a Γ-tree T of outdegree at most mT1,T2 .

It remains to be shown that each step of the algorithm can be carried out effectively and that the algorihm yields the 2EXPTIME upper bound stated in Theorem 4. We start with the former. The proof of the following lemma relies on the fact that satisfiability in ALCQI relative to TBoxes can be decided in EXPTIME [10].

Lemma 14 It can be checked in 2-exponential time (in the size of T1, T2) whether a (root or internal) pair can be obtained in one step from a set R of realizable internal pairs with |R| ≤ mT1,T2 .

Suppose TBoxes T1 and T2, and a signature Γ ⊆ sig(T1) are given.

1. Determine the set Rr0 of root pairs realized by singleton Γ-trees. If Rr0 = ∅, then reject the input (because T1 is not satisfied in any model). If Rr0 contains a root pair (t, U) such that U = ∅, then accept. Else,
2. Determine the set R0 of internal pairs realizable by singleton Γ-trees. If R0 = ∅, then reject the input. Else,
3. Generate the sequence R1,R2, . . . of sets of internal pairs such that

where R′i is the set internal pairs which can be obtained from some non-empty subset of Ri of cardinality not exceeding mT1,T2 in one step. This is done until Ri = Ri ∪ R′i . Then accept the input if there exists a root pair (t,U) with U = ∅ which can be obtained in one step from some subset of Ri of cardinality not exceeding mT1,T2 . If no such root pair exists, reject the input.

Figure 2: Algorithm for non-conservativeness w.r.t. Γ.

The number of internal pairs is bounded double exponentially in the size of |T1 ∪ T2|. Therefore, the third step of the algorithm stabilizes after at most double exponentially many rounds. Together with Lemma 14, it follows that our algorithm is a 2-ExpTime one.

Theorem 15 The algorithm in Figure 2 accepts input T1, T2, Γ iff T1 ∪ T2 is not a conservative extension of T1 w.r.t. Γ. It runs in 2-exponential time.

To show the upper bound on the size of witness concepts stated in Theorem 4, we proceed as follows: first, we observe that if the algorithm finds a realizable root pair (t, ∅), then this pair is realized by a Γ-tree of at most double exponential depth and single exponential outdegree. Second, we show how to convert such a Γ-tree into a witness concept of three-exponential size.

4 Undecidability in ALCQIO

We show that conservative extensions are undecidable in ALCQIO. The proof is by a reduction of the following undecidable tiling problem.

Definition 16 A domino system D = (T, H, V, R, L, T, B) consists of a finite set T of tiles, horizontal and vertical matching relations H, V ⊆ T × T , and sets R, L, T, B ⊆ T of right tiles, left tiles, top tiles, and bottom tiles. A solution to D is a triple (n,m, τ) where n,m ∈ and τ : {0, . . . , n - 1} × {0, . . . ,m - 1} → T such that the following hold:

1. (τ(i, j), τ(i +1, j)) ∈ H, for all i < n and j ≤m;
2. (τ(i, j), τ(i, j +1)) ∈ V , for all i ≤ n and j <m;
3. τ(0, j) ∈ L and τ(n, j) ∈ R, for all j ≤m;

Using proof methods from [11], it is easy to show that it is undecidable whether a given domino system D has a solution. We show how to convert a domino system D into TBoxes T1 and T2 such that D has a solution iff T1 ∪ T2 is not a conservative extension of T1. In particular, models of witness concepts will correspond to solutions of D.

Let D = (T,H, V,R,L, T,B) be a domino system. The TBox T1 uses the following signature: an indidual name o, role names rx and ry, concept names top, bottom, left, and right and each element of T as a concept name. The TBox T1 contains the following:

• The roles rx, ry, and their inverses are functional:

• Every position in the n ×m grid is labeled with exactly one tile and the matching conditions are satisfied:

• The concepts left, right, top, bottom mark the boundaries of the grid in the expected way:

and similarly for left, top, and bottom.

• The individual name o marks the origin:

The TBox T2 introduces two new concept names Q and P . It contains the following two concept inclusions:

The idea behind this definition of T2 is to enforce that models I of witness concepts are such that (i) there is no infinite outgoing rx/ry-path starting at oI and (ii) rx and ry commute in the connected part of I rooted at oI . This is achieved as follows: if (i) is violated, then we can find an assignment of Q in I that satisfies T2. Similarly, if (ii) is violated, then we can find an assignment of (Q and) P in I that satisfies T2.

It can be checked that, as intended, D has a solution iff T1 ∪ T2 is not a conservative extension of T1. Here, we only show how to construct a witness concept in the case that D has a solution. Such a witness concept C has to ensure that for all models I of C and T1, the connected part of I rooted at oI is isomorphic to the n×m-grid.

For every word w ∈ {rx, ry}∗ , denote by ←- w the word that is obtained by reversing w and then adding ·- to each symbol. Let |w|r denote the number of occurrences of the symbol r in w. Now, C is the conjunction of

and for every w ∈ {rx, ry}∗ such that |w|rx < n and |w|ry < m, the concept

where ∃w.D abbreviates ∃r1. · · · ∃rk.D if w = r1 · · · rk. It is readily checked that C enforces an n×m-grid as required.

Theorem 17 In ALCQIO, conservative extensions are undecidable.

Note that the theorem applies even to the case where Γ = sig(T1) and we allow (⩽ 1 r ⊤) as the only form of number restriction.

5 Conclusion

Although the high computational complexity suggests that efficient tools for deciding conservative extensions will be difficult to attain, our results and techniques lay theoretical foundations that are important for practical applications of conservative extensions. These could be based on approximations, semi-decision procedures, and on syntactic restrictions in a normative framework such as [3]. Finally, transitive roles are a main ingredient of DLs underlying OWL-DL. It remains an important open problem to investigate conservative extensions for DLs containing transitive roles and role hierarchies.