Beweistheoretische Anwendungen von CERES

01.01.2010 - 30.04.2012
Forschungsförderungsprojekt
Beweistheoretische Anwendungen der CERES Methode Alexander Leitsch Kurzfassung 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.

Personen

Projektleiter_in

Projektmitarbeiter_innen

Institut

Förderungsmittel

  • Fonds zur Förderung der wissenschaftlichen Forschung (FWF) (National) Fonds zur Förderung der wissenschaftlichen Forschung (FWF) Fördergeber Typ Forschungsförderungsinstitutionen

Forschungsschwerpunkte

  • Information and Communication Technology

Schlagwörter

DeutschEnglisch
Beweistheorieproof analysis
automatische Deduktionautomated deduction