Titel:       Verbindung von 'computation' und 'deduction' im ISAC-System
Vortragender:Mathias Lehnfeld

Das ISAC-Projekt entwickelt einen Mathematik Assistenten aufbauend auf  
den Theoremprover Isabelle. Der Kern des ISAC-Systems ist ein  
Lucas-Interpreter, der automatisch Benutzerführung für schrittweises  
Problemlösen erzeugt: Der nächste Schritt wird von einem Programm  
berechnet ('computation'); 'deduction' wird gefordert, wenn der Benutzer  
eine Formel eingibt (die Ableitbarkeit der Formel aus dem Kontext ist zu  
beweisen).

Die Aufgabenstellung im Rahmen des Projektpraktikums besteht darin, das  
in Isabelle verfügbare Konzept 'context' in den Lucas-Interpreter  
einzubauen. Isabelles 'contexts' verallgemeinern das Konzept  
'environment', idem sie dieses zusammen mit Prädikaten und Setups von  
Beweistools in einer Datenstruktur zusammenfassen. Somit enthält ein  
'context' alle lokal notwendigen Daten, um einen Block in einem Beweis  
speziell zu  bearbeiten. In ISAC werden nun 'contexts' schrittweise  
während Spezifikation und Rechnung aufgebaut.

Der Vortrag beschreibt die zugrundeliegenden Konzepte, die besonderen  
Herausforderungen in dieser Re-Engineering-Aufgabe und die Auswirkungen  
der Design- und Implementations-Arbeit. Als besondere Auswirkungen sind  
hervorzuheben:
# Benutzereingaben werden nun mithillfe der 'contexts' einer  
automatischen Typinferenz unterzogen. Infolgedessen muss ein  
Typeconstraint, wenn überhaupt, nur einmal eingegeben werden.
# Isabelles Beweistools werden nun an den entsprechenden Stellen alle  
Daten in 'contexts' bereitgestellt, die sie zum Beweisen von  
'preconditions' und 'postconditions' benötigen, und auch zum  
Verifizieren von Benutzereingaben.

Damit wird sowohl die Verbindung von 'deduction' und 'computation' in  
ISAC vorangetrieben als auch die Integration von Isabelle und ISAC; die  
Leistungsfähigkeit des experimentellen ISAC-Systems wird unmittelbar  
verbessert und künftige Verbesserungen werden entscheidend vorbereitet.