Beweistransformationen mittels Schnittelimination in der intuitionistischen Logik

Seit der Zeit der alten Griechen sind Beweise das wissenschaftliche Rückgrat der Mathematik. Diese sind nicht einfach nur Verifikationen von Sätzen, sondern vielmehr Quellen der Einsicht, wie auch von Algorithmen und mathematischen Methoden. In der mathematischen Kultur spielen Beweistransformationen eine zentrale Rolle.Vor allem die Transformation von Beweisen in elementare Beweise (was formal der Schnittelimination entspricht) ermöglicht die Extraktion von Schranken, Algorithmen, und schliesslich auch Programmen. In mehreren FWF-Projekten wurde ein Programm zur automatischen Schnittelimination auf der Basis der Methode CERES (cut-elimination by resolution) erarbeitet. Dieses Programm wurde bereits erfolgreich auf die Analyse interessanter mathematischer Beweise angewendet. Die Effizienz von CERES beruht auf dem Gebrauch automatischer Beweiser welche den wahren Kern der Methode bilden. CERES wurde für klassische Logik (erster und höherer Stufe) definiert, sowie für einige Klassen der mehrwertigen Logik. Die Hauptaufgabe des Projektes ist die Erweiterung von CERES auf intuitionistische Logik (betrachtet man das Problem der Beweisanalyse in der Mathematik dann ist die intuitionistische, neben der klassischen, die wichtigste Logik). In der Tat ensteht bei Anwendung der klassischen CERES-Methode (im Gegensatz zur Methode von Gentzen) vielfach aus einem intuitionistischen ein klassischer schnittfreier Beweis, was eine Anpassung der Methode notwendig macht. Das Ziel ist die Entwicklung zweier CERES-Typ Methoden für intuitionistische Logik; die erste (mehr konservative) sollte auf einem Resolutionskalkül für die intuitionistische Logik basieren und vom klassischen CERES nur minimal abweichen, die zweite sollte für die Beweissuch-Phase verschiedene Kalküle (z.B. auch LJ selbst) verwenden. Darüber hinaus ist eine tiefgehende Analyse geplant, wann und wie klassische schnittfreie Beweise, welche durch die Anwendung des klassischen CERES auf einen intuitionistischen Beweis entstehen, in intuitionistische transformiert werden können. Die entwickelten Methoden sollen implementiert und auf einen mathematischen Beweis aus der linearen Algebra angewendet werden. Die intuitionistische Logik besitzt (über den Curry-Howard Isomorphismus zwischen natürlichem Schliessen und dem typisierten lambda-Kalkül) eine natürliche computationale Interpretation. Es ist daher geplant, die Auswirkung von intuitionistischem CERES auf die Ausführung funktionaler Programme (über die zugehörige Beweistransformation) zu untersuchen; in der Tat könnte die Ausführung eines Programmes mittels CERES viel effizienter als die beta-Reduktion sein. Aus der theoretischen und praktischen Arbeit an der Methode sollte letztlich ein System für automatische und semi- automatische Beweistransformation in intuitionistischer Logik (wie es bereits für die klassische Logik existiert) enstehen, welches für Mathematiker als Hilfsmittel zur Analyse und Entwicklung mathematischer Beweise dienen sollte.

Schnitt-Elimination ist eine Technik der Beweistransformation welche dazu dient relevante Information aus Beweisen zu gewinnen (dabei kann es sich um einen Repräsentanten eines existentiellen Satzes oder um eine berechenbare Funktion handeln). Schnittelimination macht implizite Information explizit und ist daher eine zentrale Technik im sogenannten proof mining. Da diese Beweistransformation sehr technisch und kompliziert ist, ist es im allgemeinen nicht möglich diese händisch auszuführen, es sei denn es handelt sich um recht einfache Beweise. Die Standard-Methode der Schnittelimination (abgeleitet aus dem berühmten Beweis von Gerhard Gentzen von 1935) basiert auf einer schrittweisen Reduktion der Beweise und ist sehr redundant und ineffizient. Die Methode CERES (Cut-Elimination by Resolution) ist eine neuere Methode zur Schnitt-Elimination welche um das Jahr 2000 entwickelt wurde; in dieser wird der gesamte Beweis analysiert und das Problem der Schnitt-Elimination auf ein Problem des Automatischen Beweisens reduziert. CERES wurde zuerst für die Logik erster Stufe definiert und weiters für die Logik höherer Stufe. Das Problem, die Methode auf die intuitionistische Logik zu erweitern (welche konstruktiver als die klassische Logik ist, potentiell mehr Information liefert, aber schwerer zu handhaben ist) wurde weitgehend gelöst. Da intuitionistische (wie auch die klassische) Logik ein zentrales Werkzeug zur Modellierung mathematischer Beweise ist, ist die Entwicklung effizienter Methoden von großem Interesse. In diesem Projekt wurde die Methode CERES auf die intuitionistische Logik erweitert und mit der traditionellen reduktiven Methode der Schnitt-Elimination verglichen. Wie schon in der klassischen Logik wurde auch hier eine bedeutende Steigerung der Effizienz erzielt. Allerdings ist die Methode viel weniger uniform und zeigt ein sehr verschiedenes Verhalten auf verschiedenen Klassen von Beweisen. Die in diesem Projekt entwickelten Methode haben auch zu einer Verbesserung der ursprünglichen CERES-Methode geführt. Das Projekt leistet einen Beitrag zum besseren Verständnis mathematischer Beweise und zur Entwicklung effizienterer Methoden zur Beweisanalyse.