Shapes of Alignments Construction, Combination, and Computation

Abstract

We present a general approach for representing and combining 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.

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 nding adequate relationships or mappings between the syntactical material of di erent 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 rst 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 institutions. This generalises earlier work of a similar spirit, brie y 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 combining alignments, compare Section 3.5, and easily covers and uni es standard alignment problems of identifying symbols from di erent ontologies or keeping symbols from di erent ontologies with the same name apart. However, it also covers more elaborate integration scenarios, for instance those based on E -connections or DDLs, where not a simple identity but a more complex relationship between symbols is established|this is presented in Section 6.

Moreover, we brie y discuss how heterogeneous ontology alignments can be represented as diagrams using the heterogeneous speci cation language HetCasl, 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 exible 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 enlargement of context):

M 0 j= 0 (') , M 0j j= ' Here, : ! 0 is a signature morphism, relating di erent signatures (or module interfaces), (') is the translation of the -sentence ' along , and M 0j 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 speci c 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 de ned as usual: T j= ' 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 rstorder logic with equality, signatures are many-sorted rst-order signatures, consisting of sorts and typed function and predicate symbols. Signature morphisms map symbols such that typing is preserved. Models are many-sorted rst-order structures. Sentences are rst-order formulas. Sentence translation means replacement of the translated symbols. Model reduct means reassembling the model's components according to the signature morphism. Satisfaction is the usual satisfaction of a rst-order sentence in a rst-order structure. 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 eld names. Signature morphisms map sorts, relation symbols and eld names. A model consists of a carrier set for each sort, and an n-ary relation for each relation symbol with n elds. A model reduction just forgets the parts of a model that are not needed. A sentence is a link (integrity constraint) between two eld names of two relation symbols. Sentence translation is just renaming. A link is satis ed in a model if for each element occurring in the source eld component of a tuple in the source relation, the same element also occurs in the target eld component of a tuple in the target relation.

Example 3. Description Logics. Signatures of the description logic ALC consist of a set B of atomic concepts and a set R of roles, while signature morphisms provide respective mappings. Models are single-sorted rst-order structures that interpret concepts as unary and roles as binary predicates. Sentences are subsumption relations C1 v C2 between concepts, where concepts follow the grammar

C ::= B j > j ? j C1 t C2 j C1 u C2 j :C j 8R:C j 9R:C Sentence translation and reduct is de ned similarly as in FOL=. Satisfaction is the standard satisfaction of description logics. ALCms is the many-sorted variant of ALC. The description logic E L restricts ALC as follows: C ::= B j > j C1 u C2 j 9R:C. SHOIN extends ALC with role hierarchies, transitive and inverse roles, (unquali ed) number restrictions, and nominals.

Example 4. Quanti ed Modal Logic. (Constant-domain) rst-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 rst-order Kripke structures. Sentences follow the grammar for FOL-sentences while adding the operator, and satisfaction is standard modal satisfaction. tu tu tu tu 3 3.1

Alignments as Diagrams

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

1

- O O1 2

O2 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 9author :> u 9title:>, etc.

The reference ontology O is a rst-order theory. It contains, among others: 8x:(Working Person(x ) ! (Tangible Thing(x ) ^ 9y:(String(y) ^ Name(x ; y)))) 8x:(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) ^

^9j:(Journal (j ) ^ Has Article(j ; a)) 2(Article(x)) = Publication(x ) We will reformulate this example as a (general) heterogeneous alignment in Section 4. tu 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 exible in one aspect: with the approach of Schorlemmer and Kalfoglou [2008 ], e.g. in rst-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 de nition p(x) , '). { More importantly, perhaps, there may be no suitable common reference ontology 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 restriction 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) { concepts 1(c) in O1 and 2(c) in O2 are identi ed for each concept c in , regardless of whether the concepts have the same name or not, and { concepts in O1 n ( 1) and O2 n ( 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 identi cation of speci c parts (namely those given through h ; 1; 2i).

V-alignments can thus deal with basic alignment problems, such as synonymy (identifying di erent symbols with the same meaning) and homonymy (separating (accidentally) identical symbols with di erent meaning)|see Figure 2. fWoman; River Bank; Financial Bank; Human Beingg

- O fWoman; =Persong

O1 fWoman; Bank; Persong 1 2

- O2 fWoman; Bank; Humang Example 6. In Figure 2, the interface h ; 1; 2i speci es that the two instances of the concept Woman as well as Person and Human are to be identi ed. This yields two concepts Woman and Human Being in the push-out ontology O obtained 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. tu However, notion such as polysemy are typically understood to relate terms that have a di erent, 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 discussing 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 ] introduce 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.

fWomang

O1 fWoman v Persong - B fPersong - O2 1 fWom=ang 2 = fPersong

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 coupling of O1 and O2; indeed, the bridge ontology is something like a super-ontology of a sub-ontology and hence can be anything. 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 requirements to (1) de ne 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: fWoman v Persong

] - O1

O1 fWoman; Bankg fWoman; Person; River Bank; Financial Bankg - O

= fPersong fPerson; Bankg

] - O2

O2 fPerson; Bankg

E -connections as a kind of extended (and heterogeneous) M-alignment will be discussed in Section 5. Compare also Example 8 below. 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 di erent 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 Adamek et al. [1990 ].

De nition 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 `modules' 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 di erent formalisms, like relation schemata, description logics, rst-order logic, and modal ( rst-order) logics, alignments of ontologies need to be constructed across di erent institutions.

Heterogeneous speci cation is based on some graph of logics and logic translations, formalised as institutions and so-called institution comorphisms, see Goguen and Rosu [2002 ]. The latter are again governed by the satisfaction condition, this time expressing that truth is invariant also under change of notation across di erent logical formalisms:

M 0 j=J ( ) (') , (M 0) j=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 attening, 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 L2signature morphism : ( 1) ! 2. Sentences, models and satisfaction in the Grothendieck institution are de ned 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 alignment. For illustrative purposes, we include the full heterogeneous theory. logic DL

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 satis es the relational scheme axioms (referential integrity constraints). Of course, this is not possible literally, but rather the ontology is mapped to rst-order logic (CASL) and then extended de nitionally to Biblio DL0 with a de nition of the database tables in terms of the ontology classes and properties (compare the speci cation above after %def). Also, Biblio RS is translated to rst-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 DL

Biblio RS

The involved signature and theory morphisms live in the Grothendieck institution. Thus, we can avoid the use of arbitrary maps i as in Schorlemmer and Kalfoglou [2008 ] and instead rely entirely on (Grothendieck) signature morphisms.

In fact, note that the above view is not provable. However, it becomes provable if an inverse of the role hasArticle is introduced and used to restrict the class Article. tu 5

E -Connections as Heterogeneous Alignments In this section, we show how the integration of ontologies via `modular languages' can be conceived of as speci c alignments. We concentrate on E-connections, but note here that DDLs [ Borgida and Sera ni, 2003 ] can be treated in exactly the same way [ Kutz et al., 2004 ].

Originally conceived as a versatile and computationally well-behaved technique 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 disjoint (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, o er an appealing compromise between expressive power and computational complexity: although powerful enough to express many interesting concepts, the coupling between the combined logics is su ciently 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 2 f1; 2g, of Si, a model of the E -connection CE (S1; S2), where E = fEg, is a structure of the form

M =

W1; W2; EM ; where EM W1 W2. The extension CM Wi of an i-concept C is de ned by simultaneous induction. For concept names C of Si, we put CM = CWi ; the inductive steps for the Booleans and function symbols of Si are standard; nally, (hEj i1 C)M = fx 2 W1 j 9y 2 CM (x; y) 2 EM ; j g (hEj i2 D)M = fx 2 W2 j 9y 2 DM (y; x) 2 EM : j g Example 9. Suppose two ontologies O1 and O2, possibly formulated in di erent 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 9has state:(Open t Closed) u 9o ers:Views; while the meaning of Window in O2 might be `something that is bulletproof glass':

Window

Glass u 9has 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 `consists of '. A concept of the form hconsists of i1 C then collects all objects of O1 that are made from something in C, while a concept hconsists of i2 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: hconsists of i2 Window1 v 9has feature:Transparent hconsists of i1 Window2 v Window1 u 9provides security :Inhabitant assuming that windows in O1 might also be made of plastic, etc. tu

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 di erent logics, but have to be build from many-sorted vocabulary, 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 di erence between DDLs and various E -connections now lies in the expressivity of the `link language' L connecting the di erent ontologies. While the link language of DDL O1

CE (O1ms; O2ms) c

O1ms

O1ms ] O2ms c

c ;

DDL(O1ms; O2ms)

O2ms c

O2 is a certain sub-Boolean fragment of many sorted ALC, the basic link language of E -connections is ALCIms.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 analysis and reasoning tools for the speci cation 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 (tawxit)h, rSelHatOioInNal ascnhde mitsess,uabslowgieclsl aEsLFaOndLmAsLanCd, aQlsSo5su(pupsionrgtisnygnMtaaxnocfhetshteerCsaysnllanguage). See the extended example in Sect. 4 for the look-and-feel of HetCasl speci cations.

W-alignment obtained with Hets.

Hets also o ers 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 pro les). As a general 5 But can be weakened to ALCms or the link language of DDLs, or strengthened to more expressive many-sorted DLs such as ALCQIms.

Heterogeneous theories grouped inside a library of speci cations 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 visualise the diagram of the ontology alignment. Figure 7 shows the diagrams of a V- and a

The construction of colimits for heterogeneous diagrams is considerably more di cult. We refer the reader to Mossakowski [2006 ]; Codescu and Mossakowski [2008 ] for a detailed analysis of su cient conditions for obtaining colimits of heterogeneous theories, and for a discussion of weaker notions that are useful in cases where heterogeneous colimits do not exist.

Fig. 8. Colimit of a V-alignment in Hets. 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). tu 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 nding theory morphisms into the Heterogeneous Tool Set. This tool, together with other known alignment tools, could then be used as a basis for nding 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 Schroder for fruitful discussions, Dominik Lucke for implementing relational schemes and DL in Hets, and Erwin R. Catesbeiana for singling out an inconsistent alignment.

References

Biblio DL0 ................ . Biblio RS0 6 6

Adamek , J. , Herrlich , H. and Strecker , G. ( 1990 ). Abstract and Concrete Categories . 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 . Birkhauser . To appear.

Euzenat , J. and Shvaiko , P. ( 2007 ). Ontology Matching . Heidelberg: Springer.

Goguen , J. and Rosu , G. ( 2002 ). Institution morphisms . Formal aspects of computing 13 , 274 { 307 .

Goguen , J. A. and Burstall , R. M. ( 1992 ). Institutions: Abstract Model Theory for Speci cation 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 . Arti cial Intelligence 156 , 1 { 73 .

Kutz , O. and Mossakowski , T. ( 2007 ). Modules in Transition: Conservativity, Composition, and Colimits . In Proc. of WoMO-07 , Whistler, Canada .

Lutz , C. , Walther , D. and Wolter , F. ( 2007 ). Conservative Extensions in Expressive 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. Futatsugi, 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 Luttich, K. ( 2007a ). The Heterogeneous Tool Set . In TACAS 2007 , volume 4424 of LNCS . Springer.

Mossakowski , T. , Maeder , C. and Luttich, 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 OntologyBased Semantic Integration . Journal of Applied Ontology . To appear.

Zimmermann , A. , Krotzsch, M. , Euzenat , J. and Hitzler , P. ( 2006 ). Formalizing Ontology Alignment and its Operations with Category Theory . In Proc. of FOIS .