Schemata und Beweise

Das Ziel dieses Projektes ist die Entwicklung einer theoretischen Grundlage zur Behandlung von Formel- und Beweis-Schemata in interaktivem (oder automatischem) Beweisen und die Verwendung dieser Schema-Kalküle zur Formalisierung und Analyse mathematischer Beweise (mittels beweis-theoretischer Transformationstechniken basierend auf Schnittelimination). Die betrachteten Schemata sind Iterations-Schemata, welche in Mathematik und Informatik allgegenwärtig sind: typische Beispiele dafür sind das Schubfach-Prinzip und Ramsey`s Theorem. Diese Schemata treten auch häufig im Kontext von Schaltkreis- und Programmverifikation auf, wo die modellierenden Formeln oft durch eine natürliche Zahl parametrisiert sind (die zum Beispiel die Anzahl der Bits oder die Größe der Daten bezeichnet). Mittels solcher Formeln logisch zu schließen ist schwierig, und bedarf häufig einer Form der mathematischen Induktion. Der Entwurf von Beweisverfahren, mit Hilfe derer solche Schlüsse automatisch gezogen werden können, würde die Ausdrucksstärke signifikant erhöhen und kürzere, informativere und strukturiertere Beweise erlauben. Die Verwendung von Iterations-Schemata ist besonders nützlich für die Formalisierung von mathematischen Beweisen, die das Subjekt dieses Antrags darstellen, da diese Schemata es erlauben, unendliche Beweissequenzen in einer sehr natürlichen und komfortablen Weise darzustellen. Diese Idee wurde im HLK/CERES System (entwickelt von Partner 2) zur Analyse von mathematischen Beweisen verwendet, um induktive Beweise zu formalisieren ohne mit einem zu ausdrucksstarken Formalismus (für die keine effiziente Beweisverfahren existieren) arbeiten zu müssen. In der aktuellen Version des Systems ist jedoch nur die Definition solcher Iterationssequenzen möglich - die resultierenden Schemata müssen, bevor sie weiter verarbeitet werden können, mittels Instanzierung zu Beweisen der Logik erster Stufe reduziert werden. Im geplanten Projekt sollen Tools entwickelt werden, um solche Sequenzen direkt auf der Objekt-Ebene behandeln zu können und insbesondere logische Schlüsse (auf automatische und/oder interaktive Weise) aus ihnen zu ziehen. Wir wollen geeignete "intermediäre" logische Formalismen definieren, deren Ausdrucksstärke größer als die der Basissprache (zum Beispiel Logik erster Stufe) aber niedriger als die von Sprachen höherer Stufe ist. Die gewonnene Sprache sollte in manchen Gesichtspunkten expressiver als die ursprüngliche sein und natürliche und prägnante Formalisierungen erlauben, aber sie sollte zur gleichen Zeit - wenn möglich - manche der guten computationalen Eigenschaften (wie zum Beispiel Entscheidbarkeit und Vollständigkeit) der ursprünglichen Sprache erhalten. Das Projekt, zentriert um Formel/Beweisschematisierung und ihre Anwendungen in der Computermathematik, steht sowohl mit der thematischen Axe "Mathematik", als auch mit der Logik, mit der Beweistheorie, und natürlich mit dem automatischen Beweisen in Beziehung. Soweit uns bekannt ist, gibt es kein anderes Projekt mit ähnlichen Zielen.

Das Hauptwerkzeug des Mathematikers ist der Beweis: Wahrheit wird durch Beweis etabliert und begründet. Die Entwicklung der mathematischen Logik im 19. und 20. Jahrhundert hat den Begriff des formalen Beweises eingeführt: ein mathematischer Beweis wird als diskretes Objekt, das algorithmisch, also durch einen Computer, manipuliert werden kann, betrachtet. Dies führte zum Studium der computational logic, die sich mit dem Studium von logischen Formalismen bezüglich ihrer Mechanisierbar- oder Automatisierbarkeit beschäftigt. Ein wichtiger Aspekt, den die computational logic studiert, ist der der Schnittelimination: es ist dies ein Algorithmus der, gegeben einen formalen Beweis, einen anderen formalen Beweis des selben Theorems berechnet, der direkt ist, also keine Umwege oder Zwischenresultate enthält. Solche Beweise sind wichtig, da nützliche Information vollständig automatisiert aus ihnen extrahiert werden kann: zum Beispiel explizite Algorithmen und obere Schranken. Ein wichtiger Aspekt der computational logic ist die Anwendung abstrakter Methoden wie der Schnittelimination auf konkrete formalisierte Beweise mit dem Ziel, neue Informationen, die in den indirekten Teilen der Beweise versteckt sind, offenzulegen.Das Wechselspiel zwischen Schnittelimination und der wichtigsten mathematischen Beweismethode, vollständiger Induktion, die den Kern unseres Verständnisses der natürlichen Zahlen darstellt, liegt im Zentrum der Forschung dieses Projekts. Es ist wohlbekannt, dass Schnittelimination in Gegenwart von Induktion im allgemeinen unmöglich ist, und das Ziel dieses Projekts war es, die Reichweite der Schnittelimination im Reich der induktiven Beweise durch die Verbindung eines neuartigen Ansatzes zur Schnittelimination mit einem neuartigen Ansatz zu induktiven Beweisen zu vergrößern: die CERES (cut-elimination by resolution) Methode, eine Schnitteliminationsmethode basierend auf Resolutionsbeweisen, die viele gute Eigenschaften hat, wurde mit dem Begriff der Beweisschemata, einem natürlichen Beweisbegriff, der einer Teilklasse der induktiven Beweise entspricht, verbunden.Im Laufe dieses Projektes wurde der vorhandene Begriff der propositionalen Formelschemata auf Beweisschemata erster Ordnung erweitert. Dieser Schritt war notwendig, um Beweise aus der mathematischen Praxis behandeln zu können. Dieser Begriff, und seine Verbindung zu induktiven Beweisen, wurden eingehend untersucht. Die technische Maschinerie der CERES Methode wurde auf den Rahmen der Beweisschemata verallgemeinert, und auf ihrer Basis wurde die CERESS (schematic CERES) Methode entwickelt und untersucht, was zum Begriff der schematischen ACNF (atomic cut normal form) führte, die eine unendliche Sequenz von schnittfreien Beweisen schematisch beschreibt. Auf der einen Seite öffnet dieses Resultat den Weg für praktische Anwendungen der CERESS Methode zur Extraktion von Information aus induktiven Beweisen der Mathematik, und auf der anderen wirft es mehrere interessante theoretische Fragen bezüglich der Beziehung zwischen schematischen Beweisen und Schnittelimination auf.