A Logical Framework for Modularity of Ontologies

1 Motivation

Modularity is a key requirement for many tasks concerning ontology design, maintenance and integration, such as the collaborative development of ontologies and the merging of independently developed ontologies into a single, reconciled ontology. Modular representations are easier to understand, reason with, extend and reuse. Unfortunately, in contrast to other disciplines such as software engineering-in which modularity is a well established notion-ontology engineering is still lacking a useful, well-defined notion of modularity.

Modern ontology languages, such as OWL [PatelSchneider et al., 2004], are logic-based; consequently, a notion of modularity needs to take into account the semantics of the ontologies and their implications.

In this paper, we propose a logic-based framework for modularity of ontologies in which we distinguish between external and local symbols of ontologies. Intuitively, the external symbols of an ontology are those that are assumed to be defined somewhere externally in other ontologies; the remaining, local symbols, are assumed to be defined within the ontology itself by possibly reusing the meaning of external symbols. Hence by merging an ontology with external ontologies we import the meaning of its external symbols to define the meaning of its local symbols.

∗This work is supported by the EU Project TONES (Thinking ONtologiES) ref: IST-007603 and by the EPSRC Project REOL (Reasoning in Expressive Ontology Languages) ref: EP/C537211/1.

To make this idea work, we need to impose certain constraints on the usage of the external signature: in particular, merging ontologies should be "safe" in the sense that they do not produce unexpected results such as new inconsistencies or subsumptions between imported symbols. To achieve this kind of safety, we use the notion of conservative extensions to define modularity of ontologies, and then prove that a property of some ontologies, called locality, can be used to achieve modularity. More precisely, we define two notions of locality for SHIQ TBoxes: (i) a tractable syntactic one which can be used to provide guidance in ontology editing tools, and (ii) a more general semantic one which can be checked using a DL-reasoner. Additionally, we present an extension of locality to the more expressive logic SHOIQ [Horrocks and Sattler, 2005]. Finally, we analyse existing ontologies and conclude that our restrictions to local TBoxes are quite natural.

When integrating independently developed ontologies, we often have to identify different symbols in the ontologies having the same intended meaning. This is a problem known as ontology matching or mapping, 1 which we are not concerned with here: we consider ontologies sharing some part of their signature, and how we can make sure that that their merge (i.e. the union of their axioms) is "well-behaved".

2 Preliminaries

We introduce the description logic SHOIQ, which provides the foundation for OWL.

A SHOIQ-signature is the disjoint union S = R ⊎ C ⊎ I of sets of role names (denoted by R, S, · · · ), concept names (denoted by A, B, · · · ) and nominals (denoted by i, j, k, · · · ). A SHOIQ-role is either R ∈ R or an inverse role R- with R ∈ R. We denote by Rol(S) the set of SHOIQ-roles for the signature S. The set Con(S) of SHOIQ-concepts for the signature S is defined by the grammar

1 The website http://www.ontologymatching.org provides extensive information about this area.

where A ∈ C, j ∈ I, C(i) ∈ Con(S), R, S ∈ Rol(S), with S a simple role, 2 and n a positive integer. We use the following abbreviations: C ⊔D stands for ¬(¬C ⊓¬D); ⊤ and ⊥ stand for A ⊔ ¬A and A ⊓ ¬A, respectively; ∀R.C and ⩽nS.C stand for ¬∃R.¬C and ¬(⩾n+1 S.C), respectively.

A SHOIQ-TBox T , or ontology, is a finite set of role inclusion axioms (RIs) R1 ⊑ R2 with Ri ∈ Rol(S), transitivity axioms Trans(R) with R ∈ R and general concept inclusion axioms (GCIs) C1 ⊑ C2 with Ci ∈ Con(S). We use A ≡ C as an abbreviation for the two GCIs A ⊑ C and C ⊑ A. The signature Sig(α) (respectively Sig(T )) of an axiom α (respectively of a TBox T ) is the set of symbols occurring in α (respectively in T ). A SHIQ-TBox is a SHOIQ-TBox that does not contain nominals.

Given a signature S = R ⊎ C ⊎ I, an S-interpretation I is a pair I = (ΔI , .I ), where ΔI is a non-empty set, called the domain of the interpretation, and .I is the interpretation function that assigns to each R ∈ R a binary relation RI ⊆ ΔI × ΔI , to each A ∈ C a set AI ⊆ ΔI , and to every j ∈ I a singleton set j I ⊆ ΔI . The interpretation function is extended to complex roles and concepts as follows:

The satisfaction relation I |= α between an interpretation I and a SHOIQ-axiom α (read as I satisfies α) is defined as follows: I |= (R1 ⊑ R2) iff RI 1 ⊆ RI 2 ; I |= Trans(R) iff RI is transitive; I |= (C ⊑ D) iff CI ⊆ DI . An interpretation I is a model of a TBox T if I satisfies all axioms in T . A TBox T implies an axiomα (written T |= α) if I |= α for every model I of T . An axiom α is a tautology if it is satisfied in every interpretation.

An S-interpretation I = (ΔI , ·I ) is an expansion of an S′ -interpretation I ′ = (ΔI ′ , ·I ′ ) if S ⊇ S′ , ΔI = ΔI ′ , and X I = X I ′ for every X ∈ S′ . The trivial expansion of I ′ to S is an expansion I = (ΔI ′ , ·I ) of I ′ such that X I = ∅ for every X ∈ S \ S′ .

3 Modularity of Ontologies

In this section, we propose a logical formalization for the notion of modularity for ontologies. In analogy to software engineering, we should be able to compose complex ontologies from simpler (modular) ontologies in a consistent and welldefined way, in particular without unintended interactions between the component ontologies. This notion of modularity would be useful for both the collaborative development of a single ontology by different domain experts, and the integration of independently developed ontologies, including the reuse of existing third-party ontologies.

2 See [Horrocks and Sattler, 2005] for a precise definition of simple roles.

In order to formulate our notion of modularity, we will distinguish between the local and external symbols of an ontology. We assume that the signature Sig(T ) of a TBox T is partitioned into two parts: the local signature Loc(T ) of T and the external signature Ext(T ) of T . To distinguish between the elements of these signatures, we will underline the external signature elements whenever used within the context of T . Intuitively, Ext(T ) specifies the concept and role names that are (or can be) imported from other ontologies, while Loc(T ) specifies those that are defined in T .

As a motivating example, imagine a set of bio-medical ontologies that is being developed collaboratively by a team of experts. Suppose that one group of experts designs an ontology G about genes and another group designs an ontology D about diseases. Now certain genes are defined in terms of the diseases they cause. For example, the gene ErbB2 is described in G as an Oncogene that is found in humans and is associated with a disease called Adrenocarcinoma 3

The concept Adrenocarcinoma is described in D, which is under the control of a different group of modelers. So, this concept is external for G, whereas the remaining concept and role names are local for G. Now one consequence of these ontologies being modularly "well-behaved" would be that the gene experts building G should not change the knowledge about diseases, even if they are using them in their axioms.

Another example is the integration of a foundational (or "upper") ontology U and a domain ontology O. Foundational ontologies, such as CYC, SUMO, 4 and DOLCE, provide a structure upon which ontologies for specific subject matters can be constructed and are assumed to be the result of an agreement between experts. Suppose that an ontology developer wants to reuse the generic concept of a Substance from U in their ontology O about Chemicals. For such a purpose, they state that the concept Organic Chemical in their chemical ontology O is more specific than Substance in U by using the axiom: Organic Chemical ⊑ Substance, where Substance ∈ Ext(O). Since foundational ontologies are well-established ontologies that one does not control and, typically, does not have complete knowledge about, it is especially important that the merge O ∪ U does not produce new logical consequences w.r.t. U-even if U changes.

In both examples, we have argued that ontology integration should be carried out in such a way that consequences of a TBox T ′ are not changed when elements of T ′ are reused in another TBox T . This property can be formalized using the notion of a conservative extension [Ghilardi et al., 2006].

Definition 1 (Conservative Extension). Let T and T ′ be TBoxes. Then T ∪T ′ is a conservative extension of T ′ if, for every axiom α with Sig(α) ⊆ Sig(T ′ ) we have T ∪ T ′ |= α iff T ′ |= α. ♦

Thus, given T and T ′ , their union T ∪ T ′ does not yield new consequences in the language of T ′ if T ∪T ′ is a conservative extension of T ′ . A useful notion of modularity, however, should abstract from the particular T ′ under consideration. In fact, the external signature should be the core notion in a modular representation as opposed to its particular definition in a particular ontology T ′ . This is especially important when T ′ may evolve, and where this evolution is beyond our control-which, for example, could well be the case when using the "imports" construct provided by OWL. Consequently, in order for T to use Ext(T ) in a modular way, T ∪T ′ should be a conservative extension of any T ′ over Ext(T ).

3 Example from the National Cancer Institute Ontology http: //www.mindswap.org/2003/CancerOntology.

4 See http://ontology.teknowledge.com.

Furthermore, it is important to ensure that, whenever two independent parts T1 and T2 of an ontology T under the control of different modelers are developed in a modular way, then T remains modular as well.

These requirements can be formalized as follows:

Definition 2 (Modularity). A set M of TBoxes T with Sig(T ) = Loc(T ) ⊎ Ext(T ) is a modularity class if the following conditions hold:

M1. If T ∈ M, then T ∪ T ′ is a conservative extension of every T ′ such that Sig(T ′ ) ∩ Loc(T ) = ∅;

Please note that our framework is independent of the DL under consideration. Also, Definition 2 does not define a modularity class uniquely, but just states conditions for being one. When the modularity class is clear from the context, we will call its elements modular ontologies.

In the next section, we focus our attention on the logic SHIQ, and show that it is possible to define a reasonable modularity class such that (1) checking its membership can be done using standard reasoning tools, (2) it has an inexpensive syntactic approximation that can be used to guide the modeling of ontologies in a modular way, and (3) our analysis of existing ontologies shows that they seem to conform "naturally" with its restrictions.

4 Modularity of SHIQ ontologies

In this section we define a particular modularity class, the class of local ontologies, which captures many practical examples of modularly developed ontologies. We first give a syntactic definition of local ontologies and then generalize it to a semantic one. Finally, we prove that our semantic definition leads to a maximal class of modular TBoxes.

Definition 2 excludes already many SHIQ-TBoxes. Property M1, in particular, implies that no modular TBox T can contain the two axioms below at the same time:

where A is a local concept name and C′1 , C′2 are constructed using Ext(T ). These axioms imply C′2 ⊑ C′1, which indeed changes the meaning of the external concepts C′ i . At this point, we are faced with a fundamental choice as to the type of axioms to disallow. Each choice leads to a different modularity class. We argue that, analogously to software engineering, where refinement is the main application of modularity, axioms of type (1) fit better with ontology integration scenarios, such as those sketched in Section 3, than axioms of type (2).

As discussed in Section 3, the external names are "imported" in order to reuse them in the definition of other concepts, and not to further constrain their meaning. Intuitively, axioms of type (1) are consistent with this idea, whereas axioms of type (2) are not.

The principal difference between these two axioms is that (2) forces the external concept C′2 to contain only instances of the local concept name A, thus bounding the size of possible interpretations of C′2 once the meaning of A is established. In contrast, (1) still (in principle) allows for interpretations of C′1 of unbounded size. Note that this argument does not prohibit all inclusion axioms between external concepts and local ones. For example, in contrast to (2), the axiom

still leaves sufficient "freedom" for the interpretation of C′2, even if the interpretation for A is fixed. In fact, this axiom is equivalent to A ⊑ ¬C′2 , and thus is of type (1).

Our choice of the types of simple axioms to disallow can be generalized to more complex axioms; for example, all axioms below should be forbidden for the reasons given above:

The last axiom is disallowed because it implies (2).

Even if an axiom does not explicitly involve the external symbols, it may still constrain their meaning. In fact, certain GCIs have a global effect and impose constraints on all elements of the models of an ontology, and thereby on the interpretation of external concepts. For example, it is easy to see that the axioms

imply (2) and the first axiom in (4) respectively. 5 These observations lead to the following definition:

Definition 3 (Locality). Let S be a SHIQ-signature and let E ⊆ S be the external signature. The following grammar defines the two sets C + E and C - E of positively and negatively local concepts w.r.t. E:

where A is a concept name from S \ E, R ∈ Rol(S), C ∈ Con(S), C+ ∈ C + E , C(i) ∈ CE , i = 1, 2, and R+ ̸∈ Rol(E). 6

A role inclusion axiom R+ ⊑ R or a transitivity axiom Trans(R+) is local w.r.t. E. A GCI is local w.r.t. E if it is either of the form C+ ⊑ C or C ⊑ C-, where C+ ∈ C + E , C- ∈ C - E and C ∈ Con(S). A SHIQ-TBox T is local if every axiom from T is local w.r.t. Ext(T ). ♦

Intuitively, the positively local concepts are those whose interpretation is bounded (i.e. its size is limited) when the interpretation of the local symbols is fixed. In this respect, they behave similarly to local concept names. Negatively local concepts are essentially negations of positively local concepts. Please, note that, given E ⊆ S, a concept written over S may be neither in C + E , nor in C - E .

5¬A1 ⊑ A2 implies ⊤ ⊑ A1⊔A2, which implies C′ ⊑ A1⊔A2. 6 Recall that ∀R.C, (⩽nR.C) and C1 ⊔C2 are expressed using

the other constructors, so they can be used in local concepts as well.

Definition 3 can be used to formulate guidelines for constructing modular ontologies, as illustrated by the following example. Moreover, Definition 3 can be used in ontology editors to detect and warn the user of an a priori "dangerous" usage of the external signature-without the need to perform any kind of reasoning.

Example 4 Suppose we are developingW, an ontology about wines, and we want to reuse some concepts and roles fromF, an independently developed ontology about food.

• F: VealParmesan ⊑MeatDish ⊓ ∃hasIngredient.Veal DeliciousProduct ⊒ ∃hasIngredient.DeliciousProduct Trans(hasIngredient)
• W: Chardonnay ⊑Wine ⊓∃servedWith.VealParmesan Rioja ⊑ Wine ⊓ ∃hasIngredient.Tempranillo RedWine ⊒ Wine ⊓ ∃servedWith.MeatDish Tempranillo ⊑ DeliciousProduct

Here Ext(W) = {hasIngredient, DeliciousProduct, VealParmesan, MeatDish} and W is local. ♦

The following Lemma shows that our notion of locality satisfies the desired properties from Definition 2.

Lemma 5 [Locality Implies Modularity]

The set of local SHIQ TBoxes is a modularity class.

To prove Lemma 5, we use the following property:

Lemma 6 Let T be a local SHIQ TBox with E = Ext(T ), and let I ′ be an E-interpretation. Then the trivial expansion I of I ′ to Sig(T ) is a model of T .

Proof. We need to show that I |= α for every α ∈ T . According to Definition 3, every α ∈ T has one of the forms: R+ ⊑ R, Trans(R+), C+ ⊑ C or C ⊑ C-, where R+ /∈ Rol(E), C+ ∈ C + E and C- ∈ C - E . To prove I |= α it is then suffices to show that (R+)I = ∅, (C+)I = ∅ and (C-)I = ΔI for each such axiom. The first property holds since I is the trivial expansion of an E-interpretation I ′ . The remaining two properties can be easily shown by induction over the definitions of C + E and C - E fromDefinition 3.

Proof of Lemma 5. Let M be a set of TBoxes Ti, each of which is local w.r.t. Ext(Ti). Property M2 from Definition 2 follows from Definition 3 since every axiom α that is local w.r.t. E is also local w.r.t. every E′ with (E′ ∩ Sig(α)) ⊆ E.

In order to prove Property M1, let T be a local SHIQTBox. Assume (⋆) T ′ ∪ T |= α for some TBox T ′ and an axiom α with Sig(α) ⊆ Sig(T ′ ) and Sig(T ′ ) ∩ Loc(T ) = ∅. We have to show that T ′ |= α.

Assume to the contrary that T ′ ̸|= α. Then, there exists a model I ′ of T ′ such that I ′ ̸|= α. Let I be the trivial expansion of I ′ to Sig(T ). Then I |= T ′ and I ̸|= α since Sig(α) ⊆ Sig(T ′ ). Additionally, by Lemma 6, I |= T . So T ∪ T ′ ̸|= α, which contradicts our assumption (⋆).

Lemma 5 tells us that, in Example 4, W ∪ F does not entail new information about food only. Even if F evolves, say by adding the axiom VealParmesan ⊑ ∃producedIn.Italy using a third ontology C of countries, W will not interfere with F. On the other hand, using the imported concepts from F allows us to derive some non-trivial properties involving the local and mixed signature of W, such as Chardonnay ⊑ RedWine and Rioja ⊑ DeliciousProduct.

As we have seen, our notion of locality from Definition 3 yields a modularity class. This class, however, is not the most general one we can achieve. In particular, there are axioms that are not local, but obviously unproblematic. For example, the axiom A′ ⊑ A′ ⊔ C′ is a tautology, but is disallowed by Definition 3 since it involves external symbols only; another example is the GCI A1 ⊔ B′ ⊑ A2 ⊔ B′ which is implied by the (syntactically) local axiom A1 ⊑ A2. The limitation of our syntactic notion of locality is its inability to "compare" concepts from the external signature.

A natural question is whether we can generalize Definition 3 to overcome this limitation. Obviously, such generalization cannot be given in terms of syntax only since checking for tautologies in the external signature necessarily involves reasoning. Since our proof of Lemma 5 relies mainly on Lemma 6, we generalize our notion of locality as follows:

Definition 7 (Semantic Locality). Let E ⊆ S. A SHIQaxiom α with Sig(α) ⊆ S is semantically local w.r.t. E if the trivial expansion I of every E-interpretation I ′ to S is a model of α. A SHIQ-TBox T is semantically local if every axiom in T is semantically local w.r.t. Ext(T ). ♦

Lemma 6 essentially implies that every syntactically local TBox is semantically local. Interestingly, both notions coincide when E = ∅ or when α is a non-trivial role inclusion axiom (not of the form R′ ⊑ R′ ) or a transitivity axiom. It is easy to check that the conditions for a modularity class in Definition 2 hold for semantic locality as well. The following proposition provides an effective way of checking whether a GCI satisfies Definition 7:

Proposition 8 Let α be a GCI and E ⊆ S. Let α′ be obtained from α by replacing every subconcept of the form ∃R.C, ⩾nR.C, and every concept name A in α with ⊥, where R /∈ Rol(E) and A /∈ E. Then α is semantically local w.r.t. E iff α′ is a tautology.

Proof. The subconcepts of the form ∃R.C, ⩾nR.C, and A are interpreted by ∅ in every trivial expansion of every E-interpretation, hence they are indistinguishable from⊥ in the context of Definition 7. Replacing all these subconcepts in α with ⊥ yields α′ with Sig(α′ ) ⊆ E, and thus Definition 7 implies that α is semantically local iff every SHIQinterpretation satisfies α′ .

As mentioned above, deciding semantic locality involves reasoning; in fact, this problem is PSPACE-complete in the size of the axiom, 7 as opposed to checking syntactic locality, which can be done in polynomial time. We expect the test from Proposition 8 to perform well in practice since the size of axioms in a TBox is typically small w.r.t. the size of the TBox, and would like to point out that it can be performed using any existing DL reasoner.

7 This is precisely the complexity of checking subsumption between SHIQ-concepts w.r.t. the empty TBox and without role inclusions and transitivity axioms [Tobies, 2001].

It is worth noting that both notions of locality provide the "black-box" behavior we are aiming at, and both involve only the ontology T and its external signature. Finally, a natural question arising is whether semantic locality can be further generalized while preserving modularity. The following lemma answers this question negatively.

Lemma 9 [Semantic Locality is Maximal]

If a SHIQ-TBox T1 is not semantically local, then there exist SHIQ-TBoxes T2 and T ′ such that T2 is local, Loc(T2) ⊆ Loc(T1), Loc(T1) ∩ Sig(T ′ ) = ∅, and T1 ∪ T2 ∪ T ′ is not a conservative extension of T ′ .

Proof. Let T1 be not semantically local, and define T2 and T ′ as follows: T2 consists of the axioms of the form A ⊑ ⊥ and ∃R.⊤ ⊑ ⊥ for every A, R ∈ Loc(T1); T ′ consists of axioms of the form ⊥ ⊑ A′ and ⊥ ⊑ ∃R′ .⊤ for every A′ ,R′ ∈ Ext(T1). Note that (i) T2 is local, (ii) for every model I of T2, we have AI = ∅ and RI = ∅ for every A, R ∈ Loc(T1) and (iii) every Ext(T1)-interpretation is a model of T ′ , and (iv) T ′ uses all symbols fromExt(T1).

In order to show that T1 ∪ T2 ∪ T ′ is not a conservative extension of T ′ , we construct an axiom α′ over the signature of T ′ such that T ′ ̸|= α′ but T1 ∪ T2 ∪ T ′ |= α′ . Since T1 is not semantically local, there exists an axiom α ∈ T1 which is not semantically local w.r.t. Ext(T1), and which we use to define α′ . If α is a role axiom of the form α = (R′ ⊑ R), we set α′ = (⊤ ⊑ ∀R′ .⊥); if α = (R′ ⊑ S ′ ) with R′ ̸= S ′ or α = Trans(R′ ), we set α′ = α; and if α is a GCI, we define α′ from α as in Proposition 8. As a result, α′ uses Ext(T1) = Sig(T ′ ) only, and T ′ ̸|= α′ since α′ is not a tautology (for the last case this follows from Proposition 8). Since T1 contains α and because of the property (ii) above for T2, we have T1 ∪T2 |= α′ , and so T1 ∪T2 ∪T ′ |= α′ .

Lemma 9 shows that semantic locality cannot be generalized without violating the properties in Definition 2. Indeed, conditionM2 implies that the union T of two local TBoxes T1 and T2 is a local TBox, and conditionM2 implies that T ∪T ′ is conservative over every T ′ with Sig(T ′ ) ∩ Loc(T ) = ∅. The results in Lemma 5 and Lemma 9 are summarized in the following theorem:

Theorem 10 A set of semantically local SHIQ TBoxes is a maximal class of modular TBoxes.

5 Modularity of SHOIQ ontologies

When trying to extend the results in the previous section to the more expressive logic SHOIQ, we soon encounter difficulties. Nominals are interpreted as singleton sets and, thus, a straightforward extension of Definition 7 fails since nominals cannot be interpreted by the empty set.

A notion of modularity, however, can still be achieved if all nominals in a TBox T are treated as external concepts; the intuitive reason for this is that the interpretation of nominals is already very constrained, and hence we have little control over it. Under this assumption, Definitions 3 and 7 can be reused for SHOIQ. Such notions of locality still allow for non-trivial uses of nominals in T . For example, the following axiom is semantically local w.r.t. E = {elvis}, even if elvis is used as a nominal:

Indeed, the trivial expansion of every E-Interpretation to S = {ElvisLover,MusicFan, likes} is a model of this axiom.

Definition 11 (Locality for SHOIQ). A SHOIQ-TBox T with Sig(T ) = R⊎C⊎I is syntactically (semantically) local w.r.t. E if T is syntactically (semantically) local w.r.t. E∪ I as in Definition 3 (Definition 7). ♦

Lemma 12 [Semantic Locality Implies Modularity] The set of semantically local SHOIQ TBoxes is a modularity class for E.

The proof is analogous to the one of Lemma 5. Unfortunately, an important use of nominals in DLs, namely ABox assertions, is non-local according to our definition. For example, the assertion elvis ⊑ Singer (typically written as elvis :Singer) is not local since elvis is treated as an external element. In fact, it is not possible to extend the definition of locality to capture assertions and retain modularity:

Proposition 13 [Assertions Cannot be Local]

For every assertion α = (i ⊑ A) there exists a syntactically local TBox T such that T ∪ {α} is inconsistent.

Proposition 13 implies that no TBox T1 containing an assertion α can be declared as local without braking either property M1 or M2 of modularity from Definition 2. Indeed, by taking T as in the proof of Proposition 13, we obtain an inconsistent merge T1 ∪ T which should be local according to M2 if T1 is local. However, no inconsistent TBox can be local since it implies all axioms and hence violates condition M1.

Even if the merge of a TBox and a set of assertions is consistent, new subsumptions over the external signature may still be entailed. For example, consider the TBox T consisting of the axiom:

which is local w.r.t. E = {green, Dark}. If we add the assertion kermit ⊑ Frog to T , then we obtain that green is a dark color (green ⊑ Dark), as a new logical consequence.

To sum up, we have shown that locality can be extended to SHOIQ, but not in the presence of assertions. An open question is whether semantic locality for SHOIQ is maximal in the sense of Lemma 9.

6 Field Study

In order to test the adequacy of our conditions in practice, we have implemented a (syntactic) locality checker and run it over ontologies from a library of 300 ontologies of various sizes and complexity some of which import each other [Gardiner et al., 2006]. 8 Since OWL does not allow to declare symbols as local or external, we have used the following "informed guess work": for an ontology T , we define the set Loc(T ) as the set of symbols in T that do not occur in the signature of the ontologies imported (directly or indirectly) using the owl:imports construct by T , and defining Ext(T ) to be the complement of Loc(T ) in Sig(T ). The owl:imports construct allows to include, in an ontology T , the axioms of another ontology T ′ published on the Web by reference. The usage of owl:imports T ′ in T produces the (logical) union T ∪ T ′ .

8 The library is available at http://www.cs.man.ac.uk/

∼horrocks/testing/

It turned out that 96 of the 300 ontologies used the owl:imports construct, and that all but 11 of these 96 ontologies are syntactically local (and hence also semantically local). From the 11 non-local ontologies, 7 are written in the OWL-Full species of OWL to which our framework does not yet apply. The remaining 4 non-localities are due to the presence of so-called mapping axioms of the form A ≡ B′ , where A ∈ Loc(T ) and B′ ∈ Ext(T ), which are not even semantically local. We were able to fix these non-localities as follows: we replace every occurrence of A in T with B′ and then remove this axiom from T . After this transformation, all 4 non-local ontologies turned out to be local.

7 Discussion and RelatedWork

In the last few years, a rapidly growing body of work has been developed under the names of Ontology Mapping and Alignment, Ontology Merging and Ontology Integration; see [Kalfoglou and M.Schorlemmer, 2003; Noy, 2004] for surveys. This field is rather diverse, has originated from different communities, and is concerned with two different problems: (i) how to (semi-automatically) detect correspondences between terms in the signatures of the ontologies to be integrated (e.g. Instructor corresponds to Professor), and, (ii) how to assess and predict the (logical) consequences of the merging. Typically, when integrating ontologies, one first solves (i) and then (ii).

Although (i) has been the focus of intensive research in the last few years [Kalfoglou and M.Schorlemmer, 2003], and tools for ontology mapping are available, to the best of our knowledge, the problem of predicting and controlling the consequences of ontology integration has been addressed only very recently in [Ghilardi et al., 2006] and [Grau et al., 2006]. In [Ghilardi et al., 2006], the authors point out the importance of the notion of a conservative extension for ontology evolution and merging, and provide decidability and complexity results for the problem of deciding conservative extensions in the basic DL ALC. In [Grau et al., 2006], the authors identify two basic ontology integration scenarios. For each of them, the authors established a set of semantic properties (including being conservative extensions) to be satisfied by the integrated ontology, and presented a set of syntactic constraints on the component ontologies to ensure the preservation of the desired semantic properties.

The results in this paper generalize those from [Grau et al., 2006], since the integration scenarios presented there are particular cases of Definition 3. Also, in contrast to both [Ghilardi et al., 2006], and [Grau et al., 2006], our notion of modularity implies a "black box" behavior with respect to the external signature: instead of considering a pair of ontologies T , T ′ , our approach takes an ontology T with specified sets of local and external symbols, and provides guarantees for the merge of T with any ontology T ′ which does not use local symbols. In contrast, the approach described in [Ghilardi et al., 2006] considers the problem of whether, for two given ALC TBoxes T , T ′ , their merge T ∪ T ′ is conservative over T ′ . It turns out that this problem is decidable in 2EXPTIME in the size of T ∪ T ′ , and thus it is significantly harder than standard reasoning tasks (such as deciding ontology consistency). A solution to the latter problem can be used to decide whether T and T ′ can be safely mergedwhich can be the case without any of them being local. If T or T ′ are changed, however, then this test would need to be repeated-which is not the case in the approach presented here (see the above discussion of its black box behavior). As a consequence, these two approaches can be used in different scenarios: ours can be used to provide guidelines for ontology engineers who want to design modular ontologies that show black box behavior, whereas the one described in [Ghilardi et al., 2006] can be used to check safe integrability for a given, fixed set of TBoxes.

Summing up, we have proposed a logic-based framework for modularity, which we have instantiated in a plausible and practically applicable way for SHIQ, and in a preliminary way for SHOIQ. We believe that our results will be useful as the foundations of tools that support both the collaborative development of complex ontologies and the integration of independently developed ontologies on the Semantic Web.