Shapes of Alignments Construction, Combination, and Computation Oliver Kutz1 , Till Mossakowski2 , and Mihai Codescu2 1 SFB/TR 8 Spatial Cognition, Bremen, Germany okutz@informatik.uni-bremen.de 2 DFKI Lab Bremen, Germany mihai.codescu@dfki.de till.mossakowski@dfki.de Abstract. We present a general approach for representing and combin- ing alignments and computing these combinations, based on the category theoretic notions of diagram, pushout, and colimit. This generalises the possible ‘shapes’ of alignments that have been introduced previously in similar approaches. We use the theory of institutions to represent heterogeneous ontologies, and show how the tool Hets can be employed to compute the colimit ontology of an alignment diagram. 1 Introduction The problem of aligning, or matching, ontologies can be essentially broken down into three sub-problems: (1) the problem of discovery, i.e., the problem of finding adequate relationships or mappings between the syntactical material of different ontologies; (2) the problem of representing such possibly rather heterogeneous ‘theory connections’; and (3) the problem of computing or constructing a new super-ontology realising the intended integration. While the first problem can be of an empirical, heuristic or statistical nature, and often requires the intervention of human experts to be adequately solved (see Euzenat and Shvaiko [2007] for a survey), (2) and (3) are purely theoretical or logical problems of adequate representation, construction, and computation. We concentrate on the latter problems and propose a general framework for representing, combining, and computing complex alignments building on the category theoretic notions of diagram and colimit and the theory of institu- tions. This generalises earlier work of a similar spirit, briefly introduced and discussed in Section 3, most notably the ‘semantic integrations’ of Schorlemmer and Kalfoglou [2008] (that we call Λ-alignments), and the V- and W-alignments of Zimmermann et al. [2006]. Our approach also gives an elegant and simple solution to the problem of com- bining alignments, compare Section 3.5, and easily covers and unifies standard alignment problems of identifying symbols from different ontologies or keeping symbols from different ontologies with the same name apart. However, it also covers more elaborate integration scenarios, for instance those based on E-con- nections or DDLs, where not a simple identity but a more complex relationship between symbols is established—this is presented in Section 6. Moreover, we briefly discuss how heterogeneous ontology alignments can be represented as diagrams using the heterogeneous specification language Het- Casl, and demonstrate how the tool Hets can be used to compute a colimit ontology of such a diagram, i.e., the required integrated super-ontology of the alignment. 2 Institutions The study of modularity principles can be carried out to a quite large extent independently of the details of the underlying logical system that is used. The notion of institution was introduced by Goguen and Burstall in the late 1970s exactly for this purpose (see [Goguen and Burstall, 1992]). Institutions capture in a very abstract and flexible way the notion of a logical system by leaving open the details of signatures, models, sentences (axioms) and satisfaction (of sentences in models). The only condition governing the behaviour of institutions is the satisfaction condition, stating that truth is invariant under change of notation (or enlarge- ment of context): M 0 |=Σ 0 σ(ϕ) ⇔ M 0 |σ |=Σ ϕ Here, σ: Σ −→ Σ 0 is a signature morphism, relating different signatures (or module interfaces), σ(ϕ) is the translation of the Σ-sentence ϕ along σ, and M 0 |σ is the reduction of the Σ 0 -model M 0 to a Σ-model. The importance of the notion of institutions lies in the fact that a surprisingly large body of logical notions and results can be developed in a way that is completely independent of the specific nature of of the underlying institution— all that is needed is captured by the satisfaction condition. We refer the reader to the literature, see Goguen and Burstall [1992]; Diaconescu [2008], for full formal details. A theory in an institution is a pair T = (Σ, Γ ) consisting of a signature Sig(T ) = Σ and a set of Σ-sentences Ax(T ) = Γ , the axioms of the theory. If T = (Σ, Γ ) is a theory and Σ 0 (resp. Γ 0 ) a signature (resp. set of sentences), we write Σ 0  T (resp. Γ 0  T ) shorthand for Σ 0 ⊆ Sig(T ) = Σ (resp. Γ 0 ⊆ Ax(T ) = Γ ). The models of a theory T are those Sig(T )-models that satisfy all axioms in Ax(T ). Logical consequence is defined as usual: T |= ϕ if all T -models satisfy ϕ. Theory morphisms are signature morphisms that map axioms to logical consequences. = Example 1. First-order Logic. In the institution FOLms of many-sorted first- order logic with equality, signatures are many-sorted first-order signatures, con- sisting of sorts and typed function and predicate symbols. Signature morphisms map symbols such that typing is preserved. Models are many-sorted first-order structures. Sentences are first-order formulas. Sentence translation means re- placement of the translated symbols. Model reduct means reassembling the model’s components according to the signature morphism. Satisfaction is the usual satisfaction of a first-order sentence in a first-order structure. t u Example 2. Relational Schemes. A signature consists of a set of sorts and a set of relation symbols, where each relation symbol is indexed with a string of sorted field names. Signature morphisms map sorts, relation symbols and field names. A model consists of a carrier set for each sort, and an n-ary relation for each relation symbol with n fields. A model reduction just forgets the parts of a model that are not needed. A sentence is a link (integrity constraint) between two field names of two relation symbols. Sentence translation is just renaming. A link is satisfied in a model if for each element occurring in the source field component of a tuple in the source relation, the same element also occurs in the target field component of a tuple in the target relation. t u Example 3. Description Logics. Signatures of the description logic ALC con- sist of a set B of atomic concepts and a set R of roles, while signature morphisms provide respective mappings. Models are single-sorted first-order structures that interpret concepts as unary and roles as binary predicates. Sentences are sub- sumption relations C1 v C2 between concepts, where concepts follow the gram- mar C ::= B | > | ⊥ | C1 t C2 | C1 u C2 | ¬C | ∀R.C | ∃R.C Sentence translation and reduct is defined similarly as in FOL= . Satisfaction is the standard satisfaction of description logics. ALC ms is the many-sorted variant of ALC. The description logic EL restricts ALC as follows: C ::= B | > | C1 u C2 | ∃R.C. SHOIN extends ALC with role hierarchies, transitive and inverse roles, (unqualified) number restrictions, and nominals. t u Example 4. Quantified Modal Logic. (Constant-domain) first-order modal logic QS5 has signatures similar to FOL= , including variables, constants, and predicate symbols, but extended by modal operators and leaving out equality. Models are constant-domain first-order Kripke structures. Sentences follow the grammar for FOL-sentences while adding the  operator, and satisfaction is standard modal satisfaction. t u 3 Alignments as Diagrams 3.1 Λ-Alignments In the approach of Schorlemmer and Kalfoglou [2008], two ontologies O1 and O2 are aligned by mapping them into a common reference ontology O as follows: theories O1 and O2 are said to be semantically integrated with respect to a theory O if (1) there exist theory interpretations α1 : O1 −→ O, α2 : O2 −→ O; (2) there exist structure reducts β1 : Mod(O1 ) −→ Mod(O), β2 : Mod(O2 ) −→ Mod(O); and (3) O is consistent. - O α1 α2 O1 O2 Fig. 1. Λ-alignment: integration into reference ontology Example 5. [From Schorlemmer and Kalfoglou, 2008, abridged] Suppose that O1 is a relational scheme. It contains author of(person,paper) and person(id,name) with a relationship from person to id. O2 is a description logic theory. It contains Article v ∃author .> u ∃title.>, etc. The reference ontology O is a first-order theory. It contains, among others: ∀x.(Working Person(x ) → (Tangible Thing(x ) ∧ ∃y.(String(y) ∧ Name(x , y)))) ∀x.(Researcher (x ) → Working Person(x )) Theory interpretations α1 , α2 can be given as follows: α1 (person(p, n)) = Researcher (p) ∧ String(n) ∧ Name(p, n) α1 (author of(p, a)) = Researcher (p) ∧ Article(a) ∧ Author (a, p) ∧ ∧∃j.(Journal (j ) ∧ Has Article(j , a)) α2 (Article(x)) = Publication(x ) We will reformulate this example as a (general) heterogeneous alignment in Sec- tion 4. t u We see the following problems with this approach3 – Allowing for arbitrary sentence maps αi is too liberal: for example, αi could map every sentence to true.4 It makes more sense to use signature morphisms and their induced sentence translation maps instead. This approach is less flexible in one aspect: with the approach of Schorlemmer and Kalfoglou [2008], e.g. in first-order logic, a predicate symbol p may be mapped to a formula ϕ. However, this is usually better captured by allowing for derived signature morphisms (see Sannella and Burstall [1983]), which here are just signature morphisms into a conservative extension (e.g. an extension by the definition p(x) ⇔ ϕ). – More importantly, perhaps, there may be no suitable common reference on- tology at hand. Rather, the common super-ontology should be constructed via a union of O1 and O2 , identifying certain concepts, while keeping others distinct. This leads to V-Alignments, discussed in the next section. 3 The aspect of logic change is ignored here, but further discussed in Section 4. 4 Schorlemmer and Kalfoglou [2008] suggest to solve this problem by a possible re- striction to conservative translations; however, even then the translation mapping every theorem in Oi to true and every non-theorem to false still is a valid but useless example. 3.2 V-Alignments Zimmermann et al. [2006] address the problem of alignment without a common reference ontology. Given ontologies O1 and O2 , an interface (for O1 , O2 ) Σ, σ1 : Σ −→ Sig(O1 ), σ2 : Σ −→ Sig(O2 ) specifies that (using informal but suggestive notation) – concepts σ1 (c) in O1 and σ2 (c) in O2 are identified for each concept c in Σ, regardless of whether the concepts have the same name or not, and – concepts in O1 \ σ(Σ1 ) and O2 \ σ(Σ2 ) are kept distinct, again regardless of whether they have the same name or not. The resulting common ontology O is not given a priori, but rather it is computed from the aligned ontologies via the interface. This computation is a pushout in the sense of category theory, which in this case is just a disjoint union with identification of specific parts (namely those given through hΣ, σ1 , σ2 i). V-alignments can thus deal with basic alignment problems, such as synonymy (identifying different symbols with the same meaning) and homonymy (separat- ing (accidentally) identical symbols with different meaning)—see Figure 2. {Woman, River Bank, Financial Bank, Human Being}  - O O1  - O2 σ1  σ2  {Woman, Bank, Person} {Woman, Bank, Human} Σ = {Woman, Person} Fig. 2. V-alignment: integration through interface Example 6. In Figure 2, the interface hΣ, σ1 , σ2 i specifies that the two instances of the concept Woman as well as Person and Human are to be identified. This yields two concepts Woman and Human Being in the push-out ontology O ob- tained along the dashed arrows. It also determines that the two instances of Bank are to be understood as homonyms, and thus generates two new distinct concepts. t u However, notion such as polysemy are typically understood to relate terms that have a different, but related meaning, and can thus not be dealt with by simply identifying symbols or keeping them apart. We will come back to this when dis- cussing E-connections as alignments in Section 5. Similarly, Zimmermann et al. [2006] themselves raise the criticism that V-Alignments do not cover the case where a concept Woman in O1 is aligned with a concept Person in O2 : here, the resulting ontology should turn Woman into a subconcept of Person. This is not directly possible with the pushout approach. 3.3 W-Alignments In order to solve this problem of V-Alignments, Zimmermann et al. [2006] intro- duce W-Alignments. They consist of two V-Alignments, using an intermediate bridge ontology B. The latter can be used to specify subconcept relationships like Woman v Person as mentioned above. {Woman} {Woman v Person} {Person}    O1  - B - O2 Σ1 Σ2 = = {Woman} {Person} Fig. 3. W-alignment: integration through bridge ontology Zimmermann et al. [2006] list the behaviour of compositions as a weak point of this approach. However, we see as the main weak point the rather loose cou- pling of O1 and O2 ; indeed, the bridge ontology is something like a super-ontology of a sub-ontology and hence can be anything. 3.4 M-Alignments Given two ontologies O1 and O2 , let us assume that we want to align them using an interface Σ. We assume that O1] and O2] are extensions (typically conservative extensions) of O1 and O2 , respectively, taking into account the possible require- ments to (1) define new symbols (in order to emulate a derived theory morphism), and (2) introduce new subconcept relationships, such as Woman v Person, as discussed above. We thus arrive at the concept of M-alignment: {Woman, Person, River Bank, Financial Bank}  - O {Woman v Person} {Person, Bank}   ] ] O1  - O2  - O1 Σ O2 ≺ ≺ = {Woman, Bank} {Person} {Person, Bank} Fig. 4. M-alignment: integration through bridge along extensions E-connections as a kind of extended (and heterogeneous) M-alignment will be discussed in Section 5. Compare also Example 8 below. 3.5 General Alignments and Their Combination Zimmermann et al. [2006] note that the composition (or better: combination) of W-alignments via pushouts resp. colimits leads to the unpleasant phenomenon that the bridge ontology of the resulting W-alignment includes the whole of one of the aligned ontologies. We think that this problem arises because colimits are used for the wrong purpose: they should be used for the computation of an integrated overall ontology, but not for the combination of alignments. Instead, the complete diagram structure of the alignments should be kept intact. This means that combination generally changes shapes of diagrams, and we hence need to generalise the notion of a (diagrammatic) alignment. The notion of diagram is formalised in category theory. It generalises the different shapes of alignments that we have seen so far. Diagrams map an index category (via a functor) to a given category of interest. They can be thought of as graphs in the category. For details, see Adámek et al. [1990]. Definition 7. A general alignment of ontologies is a diagram of theories such that the nodes are subdivided into ontology nodes and interface nodes. Now, combination of alignments is basically union of the diagrams. Further details may be found in Kutz and Mossakowski [2007], where also the problem of proof-theoretic and model-theoretic conservativity in diagrams is studied, a problem area that is extremely important when considering ontologies as ‘mod- ules’ of other ontologies, cf. Lutz et al. [2007]; Cuenca Grau et al. [2008]. 4 Heterogeneous Alignments As Schorlemmer and Kalfoglou [2008] argue convincingly, since ontologies are being written in many different formalisms, like relation schemata, description logics, first-order logic, and modal (first-order) logics, alignments of ontologies need to be constructed across different institutions. Heterogeneous specification is based on some graph of logics and logic trans- lations, formalised as institutions and so-called institution comorphisms, see Goguen and Roşu [2002]. The latter are again governed by the satisfaction con- dition, this time expressing that truth is invariant also under change of notation across different logical formalisms: M 0 |=JΦ(Σ) αΣ (ϕ) ⇔ βΣ (M 0 ) |=IΣ ϕ. Here, Φ(Σ) is the translation of signature Σ from institution I to institution J, αΣ (ϕ) is the translation of the Σ-sentence ϕ to a Φ(Σ)-sentence, and βΣ (M 0 ) is the translation (or perhaps: reduction) of the Φ(Σ)-model M 0 to a Σ-model. The so-called Grothendieck institution is a technical device for giving a semantics to heterogeneous theories involving several institution [see Diaconescu, 2002; Mossakowski, 2002]. The Grothendieck institution is basically a flattening, or disjoint union, of the logic graph. A signature in the Grothendieck institution consists of a pair (L, Σ) where L is a logic (institution) and Σ is a signature in the logic L. Similarly, a Grothendieck signature morphism (ρ, σ) : (L1 , Σ1 ) → (L2 , Σ2 ) consists of a logic translation ρ = (Φ, α, β): L1 −→ L2 plus an L2 - signature morphism σ: Φ(Σ1 ) −→ Σ2 . Sentences, models and satisfaction in the Grothendieck institution are defined in a componentwise manner. Example 8. Recall Example 5 of a Λ-alignment. The kind of integration required here can be dealt with much more elegantly as a heterogeneous general align- ment. For illustrative purposes, we include the full heterogeneous theory. logic DL spec Biblio_DL = Class: Researcher SubclassOf: name some Thing Class: Article SubclassOf: author some Thing, title some Thing Class: Journal SubclassOf: name some Thing, hasArticle some Thing, impactFactor some Thing end logic Rel spec Biblio_RS = Tables person(key id:integer, name:string) author_of(person, paper:integer) paper(key id:integer,title:string,published_in:integer) journal(key id:integer,name:string,impact_factor:float) Relationships author_of[person] -> person[id] one_to_many author_of[paper] -> paper[id] one_to_many paper[published_in] -> journal[id] one_to_many end logic CASL view Biblio_RS_in_DL : Biblio_RS to { Biblio_DL with logic DL -> CASL then %def preds journal(j,n,f:Thing) <=> Journal(j) /\ name(j,n) /\ impactFactor(j,f); paper(a,t,j:Thing) <=> Article(a) /\ Journal(j) /\ hasArticle(j,a) /\ title(a,t); author_of(p,a:Thing) <=> Researcher(p) /\ Article(a) /\ author(p,a); person(p,n:Thing) <=> Researcher(p) /\ name(p,n) } = logic RelationalScheme -> CASL end Here, Biblio DL is a DL ontology about bibliographical information, and Biblio RS is the scheme of a related relational database. The view Biblio RS in DL states that the ontology satisfies the relational scheme axioms (referential integrity constraints). Of course, this is not possible literally, but rather the ontology is mapped to first-order logic (CASL) and then extended definitionally to Biblio DL0 with a definition of the database tables in terms of the ontology classes and properties (compare the specification above after %def). Also, Biblio RS is translated to first-order logic, yielding Biblio RS0 , and so the view shown in Fig. 5 as a dotted line expresses a theory morphism from Biblio RS0 to Biblio DL0 . Biblio DL0  ................. Biblio RS0 6 6 Biblio DL Biblio RS Fig. 5. A heterogeneous general alignment The involved signature and theory morphisms live in the Grothendieck in- stitution. Thus, we can avoid the use of arbitrary maps αi as in Schorlemmer and Kalfoglou [2008] and instead rely entirely on (Grothendieck) signature mor- phisms. In fact, note that the above view is not provable. However, it becomes prov- able if an inverse of the role hasArticle is introduced and used to restrict the class Article. t u 5 E-Connections as Heterogeneous Alignments In this section, we show how the integration of ontologies via ‘modular languages’ can be conceived of as specific alignments. We concentrate on E-connections, but note here that DDLs [Borgida and Serafini, 2003] can be treated in exactly the same way [Kutz et al., 2004]. Originally conceived as a versatile and computationally well-behaved tech- nique for combining logics [Kutz et al., 2004], E-connections have also been adopted as a framework for the integration of ontologies in the Semantic Web [Cuenca-Grau et al., 2006]. The general idea behind this combination method is that the interpretation domains of the connected logics are interpreted by dis- joint (or sorted) vocabulary and interconnected by means of link relations. The language of the E-connection is then the union of the original languages enriched with operators capable of talking about the link relations. E-connections, just as DLs themselves, offer an appealing compromise between expressive power and computational complexity: although powerful enough to express many interesting concepts, the coupling between the com- bined logics is sufficiently loose for proving general results about the transfer of decidability: if the connected logics are decidable, then their connection will also be decidable. We here introduce E-connections only by way of an informal but suggestive example, for full details refer to [Kutz et al., 2004]. Given interpretations Wi = (Wi , .Wi ), i ∈ {1, 2}, of Si , a model of the E-con- nection C E (S1 , S2 ), where E = {E}, is a structure of the form M = W1 , W2 , E M , where E M ⊆ W1 × W2 . The extension C M ⊆ Wi of an i-concept C is defined by simultaneous induction. For concept names C of Si , we put C M = C Wi ; the inductive steps for the Booleans and function symbols of Si are standard; finally, 1 (hEj i C)M = {x ∈ W1 | ∃y ∈ C M (x, y) ∈ EjM }, 2 (hEj i D)M = {x ∈ W2 | ∃y ∈ DM (y, x) ∈ EjM }. Example 9. Suppose two ontologies O1 and O2 , possibly formulated in different DLs S1 and S2 , contain the concept Window. Now, ontology O1 might formalise functionalities of objects found in buildings, while ontology O2 might be about the properties of materials of such objects. The intended relation between the two instances of Window might now be one of polysemy (meaning variation), i.e., Window in O1 involves ‘something with views that can be open or closed’: Window v ∃has state.(Open t Closed) u ∃offers.Views, while the meaning of Window in O2 might be ‘something that is bulletproof glass’: Window ≡ Glass u ∃has feature.Bulletproof. A systematic integration of these two ontologies could now require a mapping of objects in O1 to the material they are made from, using a link relation 1 ‘consists of ’. A concept of the form hconsists of i C then collects all objects of 2 O1 that are made from something in C, while a concept hconsists of i D collects the materials in O2 some object in D consists of. A sensible alignment between the two instances of Window could now be formalised in E-connections as: 2 hconsists of i Window1 v ∃has feature.Transparent 1 hconsists of i Window2 v Window1 u ∃provides security .Inhabitant assuming that windows in O1 might also be made of plastic, etc. t u As should be clear from the discussion so far, E-connections can essentially be considered as many-sorted heterogeneous theories: component ontologies can be formulated in different logics, but have to be build from many-sorted vo- cabulary, and link relations are interpreted as relations connecting the sorts of the component logics (compare Baader and Ghilardi [2007] who note that this is an instance of a more general co-comma construction). The main difference between DDLs and various E-connections now lies in the expressivity of the ‘link language’ L connecting the different ontologies. While the link language of DDL E ms ms ms ms C (O1 , O2 ) DDL(O1 , O2 )  - ms ms O1 ] O2  - ms c c ms O1 O2   - - c c O1 ∅ O2 Fig. 6. E-connections many-sorted: extension of an M-alignment is a certain sub-Boolean fragment of many sorted ALC, the basic link language of E-connections is ALCI ms .5 Such many-sorted theories can easily be represented in a diagram as shown in Figure 6, showing an extension of an M-alignment. 6 Computation of Alignments The Heterogeneous Tool Set Hets [Mossakowski et al., 2007a,b] provides analy- sis and reasoning tools for the specification language HetCasl, a heterogeneous extension of Casl supporting a wide variety of logics [CoFI (The Common Framework Initiative), 2004; Bidoit and Mosses, 2004]. In particular, OWL-DL (with SHOIN and its sublogics EL and ALC, also supporting Manchester syn- tax), relational schemes, as well as FOLms and QS5 (using syntax of the Casl language). See the extended example in Sect. 4 for the look-and-feel of HetCasl specifications. Heterogeneous theories grouped inside a library of specifications are represented in Hets as graphs which can be displayed in a GUI window. Thus, by specifying ontologies and the mappings between them in a HetCasl library, we can Fig. 7. Alignment diagrams in Hets. visualise the diagram of the ontology alignment. Figure 7 shows the diagrams of a V- and a W-alignment obtained with Hets. Hets also offers an algorithmic method for computing colimits of theories in various logics, based on an implementation for computing colimits of arbitrary sets, which is further applied to sets of signature symbols, like sorts, operation and predicate symbols (the latter two divided according to profiles). As a general 5 But can be weakened to ALC ms or the link language of DDLs, or strengthened to more expressive many-sorted DLs such as ALCQI ms . strategy, names are kept identical to their original as far as possible (see the example below). If this is not possible, the common origin of symbols is indicated by a (shared) number appended to their name. Example 10. Considering the V-alignment introduced in Example 6, Figure 8 presents the Hets concept graphs of the theories combining it, as well as the one of the push-out ontology obtained with Hets (the top one). t u The construction of co- limits for heterogeneous di- agrams is considerably more difficult. We refer the reader to Mossakowski [2006]; Codescu and Mossakowski [2008] for a detailed analysis of sufficient conditions for obtaining colimits of hetero- geneous theories, and for a discussion of weaker notions that are useful in cases where heterogeneous colimits do Fig. 8. Colimit of a V-alignment in Hets. not exist. 7 Discussion and Outlook We have introduced an abstract framework of general alignments that remedies shortcomings of similar frameworks that have been discussed in the literature. The framework allows for a systematic and conceptual analysis of approaches that were previously considered rather disparate. More importantly, it makes possible generic algorithms for heterogeneous alignment problems, as have been implemented in the Heterogeneous Tool Set. An essential prerequisite for the representation of alignments as diagrams is of course the discovery of alignment mappings of various kinds. While this was not the subject of this paper, we work on integrating a tool for finding theory morphisms into the Heterogeneous Tool Set. This tool, together with other known alignment tools, could then be used as a basis for finding alignment diagrams. Acknowledgements Work on this paper has been supported by the Vigoni program of the DAAD, by the DFG-funded collaborative research center SFB/TR 8 Spatial Cognition, and by the German Federal Ministry of Education and Research (Project 01 IW 07002 FormalSafe). We thank John Bateman, Joana Hois, and Lutz Schröder for fruitful discus- sions, Dominik Lücke for implementing relational schemes and DL in Hets, and Erwin R. Catesbeiana for singling out an inconsistent alignment. Bibliography Adámek, J., Herrlich, H. and Strecker, G. (1990). Abstract and Concrete Cate- gories. Wiley, New York. Baader, F. and Ghilardi, S. (2007). Connecting Many-Sorted Theories. The Journal of Symbolic Logic 72, 535–583. Bidoit, M. and Mosses, P. D. (2004). Casl User Manual . LNCS Vol. 2900 (IFIP Series). Springer. Freely available at http://www.cofi.info. Borgida, A. and Serafini, L. (2003). Distributed Description Logics: Assimilating Information from Peer Sources. Journal of Data Semantics 1, 153–184. Codescu, M. and Mossakowski, T. (2008). Heterogeneous colimits. In Workshop on Modeling, Validation and Heterogeneity (MoVaH-08). Lillehammer, Norway, April 9 2008. CoFI (The Common Framework Initiative) (2004). Casl Reference Manual . LNCS Vol. 2960 (IFIP Series). Springer. Freely available at http://www.cofi.info. Cuenca Grau, B., Horrocks, I., Kazakov, Y. and Sattler, U. (2008). Modular Reuse of Ontologies: Theory and Practice. JAIR 31, 273–318. Cuenca-Grau, B., Parsia, B. and Sirin, E. (2006). Combining OWL Ontologies Using E-Connections. Journal of Web Semantics 4, 40–59. Diaconescu, R. (2002). Grothendieck institutions. Applied Categorical Structures 10, 383–402. Diaconescu, R. (2008). Institution-independent Model Theory. Birkhäuser. To ap- pear. Euzenat, J. and Shvaiko, P. (2007). Ontology Matching. Heidelberg: Springer. Goguen, J. and Roşu, G. (2002). Institution morphisms. Formal aspects of computing 13, 274–307. Goguen, J. A. and Burstall, R. M. (1992). Institutions: Abstract Model Theory for Specification and Programming. Journal of the ACM 39, 95–146. Kutz, O., Lutz, C., Wolter, F. and Zakharyaschev, M. (2004). E-Connections of Abstract Description Systems. Artificial Intelligence 156, 1–73. Kutz, O. and Mossakowski, T. (2007). Modules in Transition: Conservativity, Com- position, and Colimits. In Proc. of WoMO-07, Whistler, Canada. Lutz, C., Walther, D. and Wolter, F. (2007). Conservative Extensions in Expres- sive Description Logics. In Proceedings of IJCAI-07 . AAAI Press. Mossakowski, T. (2002). Comorphism-based Grothendieck logics. In K. Diks and W. Rytter, eds., Mathematical Foundations of Computer Science, volume 2420 of LNCS . Springer, pages 593–604. Mossakowski, T. (2006). Institutional 2-cells and Grothendieck institutions. In K. Fu- tatsugi, J.-P. Jouannaud and J. Meseguer, eds., Algebra, Meaning and Computation. Essays Dedicated to Joseph A. Goguen, LNCS 4060. Springer. Mossakowski, T., Maeder, C. and Lüttich, K. (2007a). The Heterogeneous Tool Set. In TACAS 2007 , volume 4424 of LNCS . Springer. Mossakowski, T., Maeder, C. and Lüttich, K. (2007b). The Heterogeneous Tool Set. In B. Beckert, ed., VERIFY 2007 , volume 259. CEUR-WS. Sannella, D. and Burstall, R. (1983). Structured theories in LCF. In Proc. 8th Colloq. on Trees in Algebra and Programming, volume 159 of Lecture Notes in Computer Science. Springer. Schorlemmer, W. M. and Kalfoglou, Y. (2008). Institutionalising Ontology- Based Semantic Integration. Journal of Applied Ontology. To appear. Zimmermann, A., Krötzsch, M., Euzenat, J. and Hitzler, P. (2006). Formalizing Ontology Alignment and its Operations with Category Theory. In Proc. of FOIS .