Publikation
IGLOO 1.0 - Eine grafikunterstützte Beweisentwicklungsumgebung
Harald Feibel
DFKI, DFKI Documents (D), Vol. 94-08, 1994.
Zusammenfassung
Das System IGLOO ist eine interaktive, grafikunterstützte Beweisentwicklungs-umgebung für Sequenzenkalküle. Es besteht aus einer Inferenz- und einer Präsentationskomponente. Die Inferenzkomponente beinhaltet einen automatischen Beweiser und einen Mechanismus zum interaktiven und taktikbasierten Beweisen. Sequenzenkalküle unterschiedlicher Logiken können zum Beweisen aktiviert werden. Die Präsentationskomponente dient zur grafischen Darstellung von Ableitungsbäumen. Das interaktive Beweisen ist durch die spezielle Grafikunterstützung ausgezeichnet. Die Taktikgenerierung in der angebotenen Taktiksprache wird durch Möglichkeiten der Beweisanalyse unterstützt. Alle Systemfunktionen werden auf der Fensteroberfläche mit der Maus ausgelöst.
Das System wurde auf einer SOLBOURNE Workstation unter UNIX in SICStus-PROLOG implementiert. X Window System bildet die Grundlage für die fensterorientierte Systemoberfläche. Der Quellcode umfaßt etwa 890 KB.