Multi-Logik Systeme

Bzgl. der heterogenen Kombination von Sprachen, Methoden und Werkzeugen sind in Bremen umfangreiche und vielversprechende Vorarbeiten, vor allem im Rahmen von COMPASS und KORSO, geleistet worden.

Junbo Liu hat, aus praktischen Erfahrungen im PROSPECTRA Projekt motiviert, ein logisches Rahmenwerk entwickelt. Im Unterschied zu "institutions" basiert sein Ansatz zur Logikunabhängigkeit nicht auf der Erfüllbarkeitsrelation sondern der Konsequenzrelation; damit kann er sowohl modell-basierte semantische als auch Beweisaspekte abdecken. Zusätzlich zu einer reinen Logikpräsentation, also der Darstellung einer Logik in einer Meta-Logik, wie sie in Logical Frameworks vorliegt werden Logikmorphismen definiert. Die Strukturierung der Theoriepräsentation führt zu einer Strukturierung der Beweiskonstruktion, damit zu getrennter Beweisführung und Wiederverwendbarkeit. Wichtig ist vor allem auch die Definitionsmöglichkeit von anwendungsspezifischen Verfeinerungsrelationen zwischen strukturierten Theorien; so kann ein korrekter Entwicklungsschritt anwendungsabhängig von spezifischen Logiken definiert werden, auch von einer (abstrakteren) Logik in eine andere (konkretere), z.B. als Transformationsschritt von einer nicht-ausführbaren in eine ausführbare Spezifikation (vgl. Duration Calculus und CSP). Eine Verfeinerungsrelation zwischen Komponenten einer Spezifikation kann zu einer Verfeinerungsrelation auf der gesamten Spezifikation erweitert werden.

Es wird erwartet, daß sich durch die Strukturierungsmöglichkeiten, z.B. Verfeinerung und Parametrisierung, das Problem der Kombination von Methoden bzw. der unterliegenden Logiken leichter lösen läßt. So ist z.B. zur Kombination von zwei Semantiken (bzw. Logiken) nicht unbedingt (wie im klassischen Ansatz) die Konstruktion einer gemeinsamen Semantik notwendig, sondern nur die axiomatische Spezifikation der Gemeinsamkeiten; beide Logiken müssen dann diese Spezifikation im Sinne der Verfeinerungsrelation erfüllen.