Evaluation der Proof-Script-Sprache für KeY

Forschungsthema:	KeY, Usability
Typ:	BA
Datum:	2017-06-01
Betreuer:	Sarah Grebing Mattias Ulbrich
Aushang:

Beschreibung

Die Interaktion zwischen Benutzer und System ist in Expertensystemen im Bereich computer-gestütztes Beweisen ein wichtiges Kriterium für eine effiziente Beweisführung. Um geeignet mit dem System interagieren zu können, muss viel Wert auf die Benutzbarkeit gelegt werden. Es gibt verschiedene Ansätze, wie der Benutzer das System beim Führen eines Beweis lenkt. Dies kann durch Klicken mit der Maus auf einer graphischen Darstellung (Proof by pointing) geschehen oder durch eine textuelle Formulierung des Beweises in sogenannten Beweisskripten (z. B. Isar, s.u.). Beide Ansätze haben ihre Vorzüge und Nachteile.
Am Lehrstuhl wurde hierzu ein Ansatz entwickelt, der es erlaubt, Mausinteraktion mit Beweisskripten zu kombinieren, so dass der Benutzer das beste aus beiden Interaktionstechniken nutzen kann und zu jedem Zeitpunkt im Beweis zwischen ihnen hin- und herwechseln kann. Dieses Konzept wurde für das interaktive Beweiser- und Verifikationssystem KeY, das am Institut entwickelt wird, prototypisch umgesetzt, indem die existierende Mausinteraktion um eine Skript-Komponente erweitert wurde. Innerhalb dieser Arbeit soll nun dieser Ansatz anhand des entwickelten Prototyps sowohl auf praktische Ausdrucksmächtigkeit, Stabilität bezüglich Wiederverwendbarkeit und dem Laden von Beweisen, sowie der sprachlichen Prägnanz für eine effiziente Beweisführung evaluiert werden. Eine Ausarbeitung in englischer Sprache wird bevorzugt, ist jedoch nicht zwingend notwendig.

Voraussetzungen

Interesse an Arbeit in forschungsnahem Umfeld. Grundkenntnisse in formalen Methoden, wie sie z. B. in der Vorlesung Formale Methoden vermittelt werden. Programmierkenntnisse in Java für die Implementierung.

Kontakt

Interesse? Weitergehende Fragen? Dann melden Sie sich unverbindlich bei uns:

• Sarah Grebing (Raum 202, Geb. 50.34)
• Dr. Mattias Ulbrich (Raum 229, Geb. 50.34)

Literatur

• Leslie Lamport (2012). How to write a 21st century proof. Journal of Fixed Point Theory and Applications 11(1):43–63.
• Yves Bertot, Gilles Kahn, and Laurent Théry (1994). Proof by pointing. TACS 1994, volume 789 of LNCS, pages 141–160. Springer.
• Markus Wenzel (1999). Isar – a generic interpretative approach to readable formal proof documents. TPHOLs 1999, volume 1690 of LNCS, pages 167–184. Springer.
• Robert Geisler, Marcus Klar, Felix Cornelius, InterACT: An interactive theorem prover for algebraic specifications, AMAST’ 96, LNCS 1101, pages 563-566, Springer