HOL-CASL, ein Beweiser für algebraische Spezifikationen

Till Mossakowski

CASL ist eine ausdrucksstarke algebraische Spezifikationssprache, die als internationaler Standard von der Common Framework Initiative (CoFI) entwickelt wurde. Wir haben eine Kodierung von CASL in HOL entwickelt, so dass Theorembeweisen in CASL mittels Isabelle/HOL (im Prinzip auch mit anderen HOL-Beweisern) möglich ist. Das HOL-CASL-System umfasst neben der Codierung von CASL in Isabelle/HOL auch IsaWin, eine graphische Benutzeroberfläche für Isabelle/HOL. Da die Isabelle-Strukturierungsmechanismen von Isabelle nicht so mächtig sind wie die von CASL, ist geplant, hier mittels des MathWeb den INKA Entwicklungsgraphen mit Isabelle zu verbinden. Schliesslich wird noch kurz auf die Verbindung zwischen CASL und dem OMDOC-Standard eingegangen.

Christoph Benzmüller, Serge Autexier,

Last modified: Thu Sep 14 09:36:04 MEST 2000