Kurzbeschreibung des Projekts

Projektnummer		Einzelprojekte  P19875
Titel		Rechnerunterstützte Analyse von induktiven Beweisen
ProjektleiterIn		LEITSCH Alexander
Bewilligungsdatum		08.05.2007
Universität / Forschungsstätte		Institut für Computersprachen Abteilung für Theoretische Informatik und Logik, Technische Universität Wien
Gebiet(e)
Keywords		cut-elimination, proof transformation, proof analysis, resolution, induction, second-order arithmetic
Homepage		http://www.logic.at/people/leitsch/

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 ACA₀ 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.