Interaktives Beweisen: Übersetzung von Beweisen, Prämissen Auswahl, Ersetzung

Das Formale Beweisen ist eine weithin anerkannte Methode um die Korrektheit von Computerprogrammen und mathematischen Theorien zu zeigen. In den letzten Jahren sind mit Hilfe verschiedenster Beweis-Assistenten, welche große Programme als korrekt beweisen konnten, viele umfassende Sammlungen von formalisierten Beweisen entstanden. Beispiele dafür sind ein optimierender C-Compiler und ein Betriebssystemkern. Ähnlich eindrucksvolle Ergebnisse wurden auch in der Mathematik erzielt, wie zum Beispiel die Beweise des Vier-Farben- Theorems, der Keplerschen Vermutung und des Odd-Order-Theorems. Trotz dieser eindrucksvollen Resultate, werden Beweis-Assistenten derzeit fast ausschließlich von Experten auf diesem Gebiet verwendet. Einer der Hauptgründe dafür ist, dass beim Arbeiten mit einem Beweis-Assistenten sehr oft Schritte von Hand bewiesen werden müssen. Doch viele dieser Schritte könnten mit Techniken aus dem Automatischen Beweisen, der Ersetzung und dem Maschinellen Lernen automatisch gelöst werden. In naher Vergangenheit sind einige Systeme entstanden, welche versuchen bestimmte Beweis-Assistenten mit anderen Gebieten der Informatik in Verbindung zu setzen. Eines dieser Systeme ist HOLyHammer, welches an der Universität Innsbruck in Kollaboration mit der Radboud Universität Nijmegen entwickelt wird. HOLyHammer ist in der Lage rund 40% der formalen Flyspeck Beweise komplett automatisch zu finden. Das Ziel dieses Projektes ist es Techniken und Werkzeuge zu entwickeln, welche es erlauben automatische Ansätze im interaktiven Beweisen zu verwenden. Dies erlaubt in weitere Folge die mechanische Konstruktion von Beweisen, welche durch den Computer verifiziert werden können. Im Speziellen wollen wir dieses Ziel wie folgt erreichen: 3.1 Beweis-Assistenten durch Methoden des Maschinellen Lernens beraten lassen. 3.2 Definition und Evaluierung einer Abbildung von Beweis-Formaten höherer Ordnung auf Formate, welche im automatischen Theorem-Beweisen, der Ersetzung und der Computer Algebra verwendet werden. 3.3 Sowie die Entwicklung von Beweismethoden basierend auf der Terminierung und Konfluenz von Ersetzung. Wir erwarten, dass die Forschung im Rahmen dieses Projektes Mathematikern sowie Informatikern, welche sich mit Formalem Beweisen beschäftigen, zu gute kommen wird. Darüber hinaus wird es neue Perspektiven auf die Kombination von Interaktivem Beweisen mit Techniken des automatischen Schließens, des Maschinellen Lernens und der Ersetzung eröffnen. Außerdem wird durch dieses Projekt das Tool HOLyHammer mächtiger. Schließlich erwarten wir, dass dieses Projekt Beweis-Assistenten benutzerfreundlicher macht und auf lange Sicht dazu beitragen wird das Formale Beweisen als Bestandteil der mainstream Mathematik und Informatik zu etablieren.

Das Formale Beweisen ist eine weithin anerkannte Methode um die Korrektheit von Computerprogrammen und mathematischen Theorien zu zeigen. In den letzten Jahren sind mit Hilfe verschiedenster Beweis-Assistenten, welche große Programme als korrekt beweisen konnten, viele umfassende Sammlungen von formalisierten Beweisen entstanden. Beispiele dafür sind ein optimierender C-Compiler und ein Betriebssystemkern. Ähnlich eindrucksvolle Ergebnisse wurden auch in der Mathematik erzielt, wie zum Beispiel die Beweise des Vier-Farben-Theorems, der Keplerschen Vermutung und des Odd- Order- Theorems. Trotz dieser eindrucksvollen Resultate werden Beweis-Assistenten derzeit fast ausschließlich von Experten auf diesem Gebiet verwendet. Einer der Hauptgründe dafür ist, dass beim Arbeiten mit einem Beweis-Assistenten sehr oft Schritte von Hand bewiesen werden müssen.Doch viele dieser Schritte könnten mit Techniken aus dem Automatischen Beweisen, der Ersetzung und dem Maschinellen Lernen automatisch gelöst werden. In naher Vergangenheit sind einige Systeme entstanden, welche versuchen bestimmte Beweis-Assistenten mit anderen Gebieten der Informatik in Verbindung zu setzen. Eines dieser Systeme ist HOLyHammer, welches an der Universität Innsbruck in Kollaboration mit der Radboud Universität Nijmegen entwickelt wird. Das Ziel dieses Projektes ist es, Techniken und Werkzeuge zu entwickeln, welche es erlauben, automatische Ansätze im interaktiven Beweisen zu verwenden. Dies erlaubt in weitere Folge die mechanische Konstruktion von Beweisen, welche durch den Computer verifiziert werden können. Im Speziellen wollen wir dieses Ziel wie folgt erreichen: (a) Beweis-Assistenten durch Methoden des Maschinellen Lernens beraten lassen. (b) Definition und Evaluierung einer Abbildung von Beweis-Formaten höherer Ordnung auf Formate, welche im automatischen Theorem-Beweisen, der Ersetzung und der Computer Algebra verwendet werden. (c) Sowie die Entwicklung von Beweismethoden basierend auf der Terminierung und Konfluenz von Ersetzung.