Rechnerunterstützte Analyse von induktiven Beweisen

Seit den antiken Griechen bilden Beweise den wissenschaftlichen Kern der Mathematik. Beweise sind aber nicht bloß Mittel zur Verifikation von Sätzen sondern enthalten auch einsichtige Begründungen, sowie neue Algorithmen und mathematische Methoden. Die Beweisanalyse und Beweistransformationen spielen in diesem Kontext eine entscheidende Rolle; Von Bedeutung ist hier insbesondere die Transformation von beliebigen Beweisen in elementare, was logisch durch Schnittelimination beschrieben wird. Sie ermöglicht die Extraktion von Schranken und Algorithmen aus Beweisen. Durch neue theoretische Methoden und die steigende Rechenkapazität von Computern wird die rechnergestützte Analyse von mathematischen Beweisen möglich. In den vorangegangenen FWF-Projekten P16264 und P17995 wurde ein Softwaresystem entwickelt, das in der Lage ist, Schnittelimination basierend auf der CERES-Methode (cut-elimination by resolution) auf realistische mathematische Beweise (formalisiert in der Logik erster Stufe) anzuwenden. Dieses System wurde bereits verwendet, um eine erfolgreiche Analyse von Fürstenbergs Beweis der Unendlichkeit der Primzahlen mit topologischen Methoden durchzuführen. Das Ziel dieses Projektes ist es, die CERES-Methode um die Behandlung der Induktion (die von grundlegender Bedeutung für mathematische Beweise ist) und Teilen der Logik zweiter Stufe zu erweitern. Dies wird nicht nur den Bereich der analysierbaren Beweise beträchtlich vergrößern, sondern auch eine einfachere Formulierung von Beweisen ermöglichen, die bereits im bestehenden System analysiert werden konnten. Um dieses Ziel zu erreichen, muss auf der einen Seite die theoretische Analyse der CERES-Methode vertieft und um die Behandlung stärkerer Systeme erweitert werden. Insbesondere planen wir das System ACA0 zu behandeln. Dabei handelt es sich um Arithmetik, deren einziger Teil zweiter Stufe die Formalisierung des Induktionsaxioms ist. Auf der anderen Seite werden wir einen Resolutionskalkül entwickeln und implementieren, der ohne Skolemisierung auskommt und auch andere Nachteile bestehender Theorem-Beweiser vermeidet, was von entscheidender Bedeutung für die Erweiterung von CERES sein wird. Weiters werden wir das neue System auf die Analyse einiger mathematischer Beweise anwenden, wobei der Satz über die Repräsentierbarkeit von Zahlen als Summe zweier Quadrate ein interessanter Kandidat ist.

Seit den antiken Griechen bilden Beweise den wissenschaftlichen Kern der Mathematik. Beweise sind aber nicht bloß Mittel zur Verifikation von Sätzen sondern enthalten auch einsichtige Begründungen, sowie neue Algorithmen und mathematische Methoden. Die Beweisanalyse und Beweistransformationen spielen in diesem Kontext eine entscheidende Rolle; Von Bedeutung ist hier insbesondere die Transformation von beliebigen Beweisen in elementare, was logisch durch Schnittelimination beschrieben wird. Sie ermöglicht die Extraktion von Schranken und Algorithmen aus Beweisen. Durch neue theoretische Methoden und die steigende Rechenkapazität von Computern wird die rechnergestützte Analyse von mathematischen Beweisen möglich. In den vorangegangenen FWF-Projekten P16264 und P17995 wurde ein Softwaresystem entwickelt, das in der Lage ist, Schnittelimination basierend auf der CERES-Methode (cut-elimination by resolution) auf realistische mathematische Beweise (formalisiert in der Logik erster Stufe) anzuwenden. Dieses System wurde bereits verwendet, um eine erfolgreiche Analyse von Fürstenbergs Beweis der Unendlichkeit der Primzahlen mit topologischen Methoden durchzuführen. Das Ziel dieses Projektes ist es, die CERES-Methode um die Behandlung der Induktion (die von grundlegender Bedeutung für mathematische Beweise ist) und Teilen der Logik zweiter Stufe zu erweitern. Dies wird nicht nur den Bereich der analysierbaren Beweise beträchtlich vergrößern, sondern auch eine einfachere Formulierung von Beweisen ermöglichen, die bereits im bestehenden System analysiert werden konnten. Um dieses Ziel zu erreichen, muss auf der einen Seite die theoretische Analyse der CERES-Methode vertieft und um die Behandlung stärkerer Systeme erweitert werden. Insbesondere planen wir das System ACA0 zu behandeln. Dabei handelt es sich um Arithmetik, deren einziger Teil zweiter Stufe die Formalisierung des Induktionsaxioms ist. Auf der anderen Seite werden wir einen Resolutionskalkül entwickeln und implementieren, der ohne Skolemisierung auskommt und auch andere Nachteile bestehender Theorem-Beweiser vermeidet, was von entscheidender Bedeutung für die Erweiterung von CERES sein wird. Weiters werden wir das neue System auf die Analyse einiger mathematischer Beweise anwenden, wobei der Satz über die Repräsentierbarkeit von Zahlen als Summe zweier Quadrate ein interessanter Kandidat ist.