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.
Ein wesentlicher Bestandteil des Beweisens ist es, schon bewiesene Gleichungen dazu zu verwenden, andere Terme umzuformen, das sogenannte Term-Rewriting. Dies geschieht in Lean momentan durch die Auflistung sogenannter Taktiken. Zwar kann der Zustand des Beweisziels nach jeder Taktik-Anwendung begutachtet werden, die Auswahl der Subterme, in denen die Umformung stattfinden soll, ist jedoch etwas umständlich.
Ziel der Arbeit ist es, Lean's Beweiszielanzeige mit der Fähigkeit auzustatten, interaktiv Subterme und Umformungs-Lemmata auszuwählen und anzuwenden.
Der dazu nötige Code wird komplett in der Sprache Lean selbst geschrieben.
Voraussetzungen
- Kenntnisse in funktionaler Programmierung
- Kenntnisse in Theorembeweisen oder abhängigen Typen werden nicht benötigt
Schlüsselworte
Lean
Betreuer
