Representations, Hierarchies and Graphs of Institutions

Für die Spezifikation und Entwicklung von Software mit formalen Methoden wurden eine ganze Reihe von Sprachen und Formalismen entwickelt. Die vorliegende Arbeit untersucht systematisch die Beziehungen zwischen Logiken totaler, partieller und Untersorten-Algebren (auch mit Prädikaten). Als Axiome sind bedingte Gleichungen und Hornformeln zugelassen.

Um diese Beziehungen untersuchen zu können, werden zunächst verschiedene mathematische Formalisierungen des Begriffs der Logik (zentral sind hier die sog. Institutions) und der Logik-Repräsentation untersucht. Letztere entsprechen unterschiedlich guten Möglichkeiten, die Modelltheorie einzubetten bzw. Beweisunterstützung wiederzuverwenden.

In diesem Rahmen werden dann fünf Graphen von Logiken erstellt, die verschiedenen Ausdrucksmächtigkeiten entsprechen. Mit Trennungsresultaten werden die fünf Graphen gegeneinander abgegrenzt.

Im abschließenden Teil des Buches geht es dann um die Kombination von Logiken mit bestimmten algebraischen Präsentationen von Institutions, genannt Parchments, und Parchment-Morphismen.