Heterogeneous Theories and the Heterogeneous Tool Set

Abstract

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