Scripting Interactive Proofs

Typ: MA / DA
Datum:
Betreuer: Sarah Grebing
Mattias Ulbrich
Bearbeiter:
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 grafischen 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.
Ihre Aufgabe in dieser Arbeit ist es, einen Ansatz zu entwickeln, 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. Nach der Einarbeitung in die Beweistechniken und Beweispräsentationen sollen Sie ein Konzept zur Integration bei der Beweistechniken entwickeln. Dieses Konzept soll für das interaktive Beweiser- und Verifikationssystem KeY, das am Institut entwickelt wird, prototypisch umgesetzt werden, indem die existierende Mausinteraktion um eine Skript-Komponente erweitert wird. 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:

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