Beweistransformation mittels Resolution

Automatisches Beweisen und Beweissuche sind seit langem wichtige Forschungsgebiete der Computationalen Logik und der Künstlichen Intelligenz. Dagegen war das Interesse an Methoden automatischer Beweistranformation bedeutend geringer. Einige dieser Methoden aber, insbesondere die Schnittelimination, sind von zentraler Bedeutung für die Extraktion algorithmischer Information aus mathematischen Beweisen und für die Transformation nicht-elementarer in kombinatorische Beweise. Die Methode CERES (cut-elimination by resolution), welche vom Autor gemeinsam mit Matthias Baaz entwickelt wurde, reduziert das Problem der Schnittelimination auf die Resolutionswiderlegung einer Menge von Klauseln. Das logische Problem der Schnittelimination wird dadurch eines des automatischen Beweisens und der Beweissuche. CERES ist in der Tat eine Methode der Beweissuche zum Zwecke der Beweistransformation. Das Hauptziel des Projektes ist der Nachweis, dass CERES nicht einfach nur eine Methode der Schnittelimination ist, sondern ein wirksames Werkzeug zur Simulation und Analyse einer grossen Klasse von Transformationsmethoden. Das Ziel einer solchen Analyse ist einerseits ein besseres Verständnis der Transformationsmethoden, andererseits aber auch deren Verbesserung. Parallel zu dieser theoretischen Untersuchung ist die Implementation von CERES und die Erweiterung der Methode im folgenden Sinne geplant: 1. durch Einführung spezifischer Resolutionsverfeinerungen und Methoden der Redundanzelimination, 2. durch Weiterentwicklung in eine Methode zur interaktiven Beweistransformation. Der letzte Schritt soll schliesslich eine Anwendung der Methode auf reale mathematische Beweise bringen. Ausserdem sollen auch substantielle mit CERES zusammenhängende beweistheoretische Probleme behandelt werden; ein solches ist das Problem der Reskolemisierung beliebiger LK-Beweise in polynomialer Zeit.