License
when quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-437
URL: http://drops.dagstuhl.de/opus/volltexte/2005/43/

Mossakowski, Till
Theoretical Foundations

Heterogeneous Theories and the Heterogeneous Tool Set

pdf-format:
Dokument 1.pdf (212 KB)


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

BibTeX - Entry

@InProceedings{mossakowski:DSP:2005:43,
  author =	{Till Mossakowski},
  title =	{Heterogeneous Theories and the Heterogeneous Tool Set},
  booktitle =	{Semantic Interoperability and Integration},
  year =	{2005},
  editor =	{Y. Kalfoglou and M. Schorlemmer and A. Sheth and S. Staab and M. Uschold},
  number =	{04391},
  series =	{Dagstuhl Seminar Proceedings},
  ISSN =	{1862-4405},
  publisher =	{Internationales Begegnungs- und Forschungszentrum f{\"u}r Informatik (IBFI), Schloss Dagstuhl, Germany},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2005/43},
  annote =	{Keywords: Heterogeneity , logic , theory mediation , tool integration}
}

Keywords: Heterogeneity , logic , theory mediation , tool integration
Seminar: 04391 - Semantic Interoperability and Integration
Issue date: 2005
Date of publication: 23.03.2005


DROPS-Home | Fulltext Search | Imprint Published by LZI