Heterogeneous Theories and the Heterogeneous Tool Set

Heterogeneous multi-logic theories arise in different contexts: they are needed for the specification of large software systems, as well as for mediating between different ontologies. This is because large theories typically involve different aspects that are best specified in different logics (like equational logics, description logics, first-order logics, higher-order logics, modal logics), but also because different formalisms are in practical use (like RDF, OWL, EML). Using heterogeneous theories, different formalims being developed at different sites can be related, i.e. there is a formal interoperability among languages and tools. In many cases, specialized languages and tools have their strengths in particular aspects. Using heterogeneous theories, these strengths can be combined with comparably small effort. By contrast, a true combination of all the involved logics into a single logic would be too complex (or even inconsistent) in many cases. We propose to use \emph{institutions} as a formalization of the notion of logical system. Institutions can be related by so-called institution morphsims and comorphisms. Any graph of institutions and (co)morphisms can be flattened to a so-called \emph{Grothendieck institution}, which is kind of disjoint union of all the logics, enriched with connections via the (co)morphisms. This semantic basis for heterogeneous theories is complemented by the heterogeneous tool set, which provides tool support. Based on an object-oriented interface for institutions (using type classes in Haskell), it implements the Grothendieck institution and provides a heterogeneous parser, static analysis and proof support for heterogeneous theories. This is based on parsers, static analysers and proof support for the individual institutions, and on a heterogeneous proof calculus for theories in the Grothendieck institution. See also the Hets web page: http://www.tzi.de/cofi/hets