Interaktive Theorembeweiser ermöglichen es, formale Beweise z.B. über Mathematik oder Programmverifikation computergestützt zu führen, d.h. der Computer überprüft nicht nur die Korrektheit des endgültigen Beweises, sondern hilft auch beim Schreiben desselben. Soll solch ein Beweis danach beispielsweise auf einer Webseite präsentiert werden, ist aber meist nur noch der reine Beweistext ohne Hilfsmittel verfügbar, was die Nachvollziehbarkeit erschwert. Alectryon ist ein neueres Tool, das versucht, solche nützlichen Metadaten aus dem Theorembeweiser Coq zu exportieren und in einer Webseite einzubetten.
Ziel dieser Arbeit ist es, Alectryon um Unterstützung für den an unserem Lehrstuhl mitentwickelten Theorembeweiser Lean 4 zu erweitern. Lean 4 wurde von Grund auf auf Erweiterbarkeit und Introspektion ausgelegt und stellt deshalb nützliche Metadaten wie einen konkreten Syntaxbaum und Beweisziele direkt zur Verfügung. Es sollte deshalb nicht nur möglich sein, Lean leicht an Alectryon anzubinden, sondern ggf. auch weitere hilfreiche Daten zu präsentieren (z.B. akkurates Syntax-Highlighting), die in anderen Theorembeweisern schwieriger zu exportieren wären.
Aufgabe:
- Exportieren der von Alectryon benötigten Metadaten aus Lean heraus (als eigenständiges Lean-Programm)
- Anpassungen von Alectryon (Python) an Lean, falls notwendig
- Ggf. sinnvolle Erweiterungen von Alectryon für Lean
Voraussetzungen
- Kenntnisse in funktionaler Programmierung und ggf. Python
- Kenntnisse in Theorembeweisen oder abhängigen Typen werden nicht benötigt
Schlüsselworte
Lean
Veröffentlichungen
Betreuer
Studenten
