Universität München,

 Institut für Informatik,

 Lehr- und Forschungseinheit für Programmierung und Softwaretechnik 

DIPLOMARBEIT

Eine Benutzeroberfläche für das Beweissystem Lego als Java-Bean

1. Die vom Beweissystem gelieferten Ergebnisstrings sollen in der in der Mathematik üblichen Form ausgegeben werden.
2. Für die Eingabe sind drei Ausbaustufen vorgesehen (abhaengig von der Zeit nach Vollendung der Punkte 1, 3, 4):
   • Eingabe in der LEGO üblichen Textform (standard).
   • Eingabe wie oben nur, da� die Symbole gleich in die mathematische Form umgewandelt werden.
   • Eingabe über einen Struktur-Editor.
3. Um mit dem System Beweise zu führen, sollen zwei Techniken implementiert werden: zum ersten "Point and Click" (d.h. durch Auswahl eines Teilterms wird die anzuwendende Regel ausgewählt) und zum zweiten "Select and Execute" (d. h. man markiert mit der Maus einen Teilterm und wählt danach ein Kommando aus, dem dieser Teilterm als Argument übergeben wird.)
4. Um die Übersichtlichkeit der einzelnen Definitionen und Deklarationen zu sichern, soll das System auch eine Modulverwaltung erhalten (d.h. jede Definition und jeder Satz ist bezüglich eines Moduls definiert bzw. bewiesen) Diese soll in ungefähr dem Browser der Isabelle-Homepage entsprechen (d.h. es soll sowohl eine Baum- als auch eine Graphdarstellung der Modulabhängigkeiten geben.)
5. Um das Arbeiten mit großen Theorien zu erleichtern ist es sinnvoll die Definitionen und Sätze in einer Datenbank zu speichern. Diese Datenbank soll folgende Suchen ermöglichen:
   • Suche nach allen Funktionen, Definitionen und Sätzen eines bestimmten Typs.
   • Suche einer Funktion, Definition und Theorems, die einen bestimmten Namen enthalten.