Algorithmische Strukturierung und Kompression von Beweisen

Beweise sind die wichtigsten Träger mathematischen Wissens. Seit dem Beginn der Forschung in der automatischen Deduktion bis zum heutigen Stand des Wissens im automatischen und interaktiven Beweisen hat sich die Fähigkeit von Computern, Beweise zu suchen, zu formalisieren und mit ihnen zu arbeiten enorm weiterentwickelt. Computergenerierte Beweise sind typischerweise analytisch, d.h. sie bestehen im Wesentlichen nur aus solchen Formeln, die bereits im zu beweisenden Theorem vorkommen. Im Gegensatz dazu sind das von Menschen geschriebene mathematische Beweise fast nie: diese sind durch die Verwendung von Lemmas hochgradig strukturiert. Daher ist es für den menschlichen Leser oft sehr schwierig, wenn nicht gar unmöglich, computergenerierte Beweise zu verstehen. In diesem Projekt sollen Algorithmen und Software entwickelt werden, die analytische Beweise durch die Berechnung nützlicher Lemmas strukturieren und abkürzen. Seit den Anfängen der strukturellen Beweistheorie ist klar wie beliebige Beweise in analytische Beweise transformiert werden können: durch Schnittelimination. Der Ansatz dieses Projekts besteht darin die Schnittelimination umzukehren. Gegeben einen analytischen Beweis (z.B. einen algorithmisch generierten) besteht die Aufgabe darin, diesen in einen kürzeren und besser strukturierten zu transformieren. Dies geschieht durch die Einführung von Schnitten, die - auf der mathematischen Ebene - Lemmas repräsentieren. Dieser Ansatz wird durch neue und wegweisende Resultate ermöglicht, die eine Verbindung zwischen der Beweistheorie und der Theorie formaler Sprachen etabliert haben. Diese Einsichten erlauben die Anwendung effizienter Algorithmen die auf formalen Grammatiken basieren auf die Strukturierung und Kompression von Beweisen. Ein erster proof-of-concept Algorithmus der diesen Ansatz verwendet ist vor kurzem publiziert worden und kann einen einzigen Schnitt mit einem Quantore generieren. Das primäre theoretische Ziel des Projekts ist es, diesen Algorithmus auf stärkere Klassen von Schnitten, bis zur vollen Logik erster Stufe, zu erweitern. Die entwickelten Algorithmen werden auch implementiert werden, um sie auf Beweise anzuwenden, z.B. als Nachbearbeitung eines automatischen Beweisers. Die Implementierung wird auf dem GAPT-Projekt basieren, das an der vorgeschlagenen Forschungsstätte entwickelt wird und ein allgemeines Framework für beweistheoretische Algorithmen zur Verfügung stellt. Das ultimative Ziel des Projekts ist es, ein Softwaresystem zu entwickeln, das als Eingabe einen analytischen Beweis akzeptiert und dann Formeln berechnet die, als Lemmas verwendet, den Eingabebeweis optimal abkürzen.

Beweise sind die wichtigsten Träger mathematischen Wissens. Seit dem Beginn der Forschung in der automatischen Deduktion bis zum heutigen Stand des Wissens im automatischen und interaktiven Beweisen hat sich die Fähigkeit von Computern, Beweise zu suchen, zu formalisieren und mit ihnen zu arbeiten enorm weiterentwickelt. Computergenerierte Beweise sind typischerweise analytisch, d.h. sie bestehen im Wesentlichen nur aus solchen Formeln, die bereits im zu beweisenden Theorem vorkommen. Im Gegensatz dazu sind das von Menschen geschriebene mathematische Beweise fast nie: diese sind durch die Verwendung von Lemmas hochgradig strukturiert. Daher ist es für den menschlichen Leser oft sehr schwierig, wenn nicht gar unmöglich, computergenerierte Beweise zu verstehen. In diesem Projekt wurden Algorithmen und Software entwickelt, die analytische Beweise durch die Berechnung nützlicher Lemmas strukturieren und abkürzen. Seit den Anfängen der strukturellen Beweistheorie ist klar wie beliebige Beweise in analytische Beweise transformiert werden können: durch Schnittelimination. Unser Ansatz besteht darin die Schnittelimination umzukehren. Gegeben einen analytischen Beweis (z.B. einen algorithmisch generierten) besteht die Aufgabe darin, diesen in einen kürzeren und besser strukturierten zu transformieren. Dies geschieht durch die Einführung von Schnitten, die - auf der mathematischen Ebene - Lemmas repräsentieren. Dieser Ansatz wird durch neue und wegweisende Resultate ermöglicht, die eine Verbindung zwischen der Beweistheorie und der Theorie formaler Sprachen etabliert haben. Diese Einsichten erlauben die Anwendung effizienter Algorithmen die auf formalen Grammatiken basieren auf die Strukturierung und Kompression von Beweisen. Das primäre theoretische Resultat dieses Projekts ist es, diesen Algorithmus auf stärkere Klassen von Schnitten zu erweitern. Die entwickelten Algorithmen wurden auch implementiert, um sie auf Beweise anzuwenden, z.B. als Nachbearbeitung eines automatischen Beweisers. Die Implementierung basiert auf dem GAPT-Projekt, das an der TU Wien entwickelt wird und ein allgemeines Framework für beweistheoretische Algorithmen zur Verfügung stellt.