IGLOO 1.0 : eine grafikunterstützte Beweisentwicklungsumgebung ; Benutzerhandbuch

Abstract

Das System IGLOO ist eine interaktive, grafikunterstützte Beweisentwicklungsumgebung 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. AIle Systemfunktionen werden auf der Fensteroberfläche mit der Maus ausgelöst. Das System wurde auf einer SOLBOURNE Workstation unter UNIX in SICStusPROLOG implementiert. X Window System bildet die Grundlage für die fensterorientierte Systemoberfläche. Der Quellcode umfaßt etwa 890 KB. IGLOO wurde am Deutschen Forschungszentrum für Künstliche Intelligenz (DFKI) in Saarbrücken innerhalb des von Prof. Dr. Wolfgang Wahlster geleiteten Projektes PHI (Planbasierte Hilfesysteme) im Rahmen einer von Dipl.-Inform. Mathias Bauer betreuten Diplomarbeit entwickelt und implementiert.