Beweistheoretische Anwendungen der CERES Methode

Seit den Griechen der Antike bilden Beweise das wissenschaftliche Rückgrat der Mathematik. Aber Beweise sind nicht nur Nachweise von Theoremen, sondern auch Quellen neuer Algorithmen und mathematischer Methoden. Beweisanalyse und -transformation spielt eine kritische Rolle in diesem Kontext; im Speziellen kann die Transformation beliebiger in elementare Beweise (in der Logik beschrieben als Schnittelimination, die - grob gesprochen - als Anwendung von Ockhams Skalpell angesehen werden kann) verwendet werden um verborgene Information explizit zu machen. Mit neuen theoretischen Methoden und der wachsenden Leistung von Computern wird die computerunterstützte Analyse von mathematischen Beweisen möglich. Zu diesem Zweck wurde die CERES Methode (Schnittelimination mittels Resolution) - im Gegensatz zu anderen Schnitteliminationsmethoden - erfolgreich eingesetzt: die prominenteste Anwendung war die Analyse von Fürstenbergs Beweis der Unendlichkeit der Primzahlen, von welchem Euklid`s elementarer Beweis gewonnen werden konnte. Die CERES Methode und das sie implementierende Softwaresystem wurden in den vorhergehenden FWF Projekten P16264, P17995 und P19875 entwickelt, verfeinert, und zu Experimenten herangezogen. Diese vergangenen Bemühungen und das hier vorgeschlagene Projekt bringen uns näher an das langfristige Ziel, computerunterstützte Beweisanalyse als Standardwerkzeug des Mathematikers zu etablieren, heran. Das erste Ziel, das in diesem Projekt bewältigt werden soll, ist die Weiterentwicklung der CERES Methode: wir wissen, dass CERES in einem gewissen Sinn stärker als die traditionellen, sogenannten reduktiven Methoden der Schnittelimination ist. Dennoch können die reduktiven Methoden in der Praxis den Vorteil haben, dass sie deterministischer als CERES sind. Unser Ziel ist daher, die reduktiven Methoden als spezifische Resolutionsverfeinerungen zu beschreiben. Solche Verfeinerungen werden nützlich sein, da es sich herausgestellt hat, dass die Suche nach einer Resolutionswiderlegung der grösste Engpass bei der Anwendung von CERES auf mathematische Beweise ist, und die Verfeinerungen den Suchraum verkleinern werden. Ausser der Steigerung der Effizienz der CERES Methode werden wir ihren Anwendungsbereich vergrössern: in ihrer derzeitigen Formulierung kann die Methode nicht auf nicht-klassische Logiken angewandt werden. Wir werden Modifikationen von CERES untersuchen, die mit solchen Logiken verwendet werden können. Das zweite Ziel ist die Anwendung der verfeinerten CERES Methode auf Probleme im Bereich der Beweisanalyse. Unter anderem werden wir mittels der Resolutionsverfeinerungen Klassen von Beweisen, die schnelle Schnittelimination zulassen, charakterisieren und die derzeitigen Resultate bezüglich CERES in Logik höherer Stufe ausweiten, was die praktische Anwendung von CERES erleichtern wird, da Beweise in dieser Logik natürlicher formalisiert werden können.

Das Ziel dieses Projekts war die Weiterentwicklung und (vor allem theoretische) Anwendung der CERES Methode. Die CERES Methode, situiert im Feld der Beweistheorie, ist ein Verfahren zur Elimination von Hilfssätzen (Lemmata) aus mathematischen Beweisen (Schnittelimination). Die durch Schnittelimination gewonnenen Lemma- freien Beweise sind computational interessant: Aus Ihnen können mathematisch wichtige Informationen (z.B. Schranken auf die Größe von Objekten) mittels einfacher Algorithmen abgelesen werden. In diesem Sinne kann die Schnittelimination als Werkzeug zur Extraktion von Information aus Beweisen verstanden werden. Das Hauptresultat dieses Projekts war die Verallgemeinerung von CERES auf CERES: Die Methode kann nun also auch auf die ausdrucksstarke Sprache der Logik höherer Stufe angewandt werden. Diese Sprache ist weit verbreitet zur Formalisierung mathematischer Beweise und wird von vielen Beweisassistenten verwendet. Die Verallgemeinerung erlaubt es also, die CERES Methode jetzt auch direkt, ohne Übersetzung, auf diese Beweise anzuwenden. Ein Korollar dieser Verallgemeinerung war die Umgehung der sogenannten Beweisskolemisierung, was einen bemerkenswerten technischen Aspekt darstellt und die praktische Anwendbarkeit der CERES Methode verbessert. Ein weiteres wichtiges Resultat war die Anwendung der CERES Methode auf die Analyse der computationalen Komplexität der Schnittelimination. Grob gesprochen wurde die Frage behandelt: "Welche Hilfssätze sind leicht, und welche schwierig aus einem Beweis zu entfernen?" Die Untersuchungen, die mithilfe der CERES Methode in diesem Projekt durchgeführt wurden, zeigten einige Klassen von Hilfssätzen auf die sich (verhältnismäßig) leicht aus Beweisen entfernen lassen. Eine praktische Konsequenz dieses Resultats ist, dass es möglich ist zu überprüfen ob ein gegebener Beweis in eine der untersuchten Klassen fällt und, falls ja, durch Anwendung der CERES Methode eine schnelle Schnittelimination durchgeführt werden kann. Die Untersuchung enthielt auch eine methodologische Komponente: Für eine der untersuchten Klassen wurde gezeigt dass die Standard- Schnitteliminationsmethode, eingeführt von G. Gentzen, sich computational sehr schlecht verhält. Damit ist bewiesen, dass eine Untersuchung der Komplexität dieser Klasse mittels der Gentzenschen Methode nicht fruchtbar sein kann, während im Gegensatz die CERES Methode gute Ergebnisse liefert. Dies zeigt die methodologische Stärke von CERES als Werkzeug für Untersuchungen in der Beweistheorie.