Hybrid Languages

für Formalisieren und Computer-gestütztes Beweisen von
System-Eigenschaften. Dabei wird ein System mit der Hilfe
von den sogenannten Transitionssystemen
(auch Kripke-Modelle genannt) modelliert.
Einige Beispiele von Systemen,
die mittels Hybridsprachen formalisiert werden
können, sind Ausführungen von Computer-Programmen,
Ablauf nebenläufiger Prozesse und KL-ONE-ähnliche
Systeme in der Wissensrepräsentation.
Hybridsprachen zeichnen sich dadurch aus, daß
verschiedene Objekt-Typen wie z.B. Aussagen über
Zustände und Zustände uniform behandelt werden.


In der Arbeit werden sogenannte Basis-Hybridsprachen untersucht,
die einerseits Erweiterungen der klassischen Modallogik sind
und andereseits Fragmenten der Logik 1. Stufe entsprechen.
Wir schlagen die ersten vollständigen Hilbert-Systeme und
Tableau-Kalküle für eine Hierarchie von solchen Formalismen
verschiedener Ausdrucksstärken vor.
Dieses Resultat löst eine der grundlegenden offenen Fragen
für Basis-Hybridsprachen.
Zusammenhänge zwischen Hybridsprachen auf der einen und
Temporallogiken und Beschreibungslogiken auf
der anderen Seite werden gezeigt.