Beweistheorie mittels beschränkter Sequenzialkalküle

Die mathematische Formalisierung eines Argumentationssystems wird als Logik bezeichnet. Logik spielt in zahlreichen Bereichen der Informatik, der mathematischen Logik, der Linguistik, der Philosophie und darüber hinaus eine herausragende Rolle. Neben der Vielfalt dieser Bereiche sind auch die Argumentationstypen, welche in den jeweiligen Szenarien zum Tragen kommen, unterschiedlich. Es gibt daher keine einheitliche Logik die in allen Szenarien anwendbar ist. Bei der Untersuchung einer Logik stellen sich mehrere wichtige Fragen. Zum Beispiel: Können wir auf effiziente Art und Weise feststellen, ob eine bestimmte Aussage (Argumentation) eine Konsequenz der Logik ist? Was ist die Komplexität eines solchen Algorithmus? Wie verhält sich die Logik zu anderen Logiken in ihrem Umfeld? Zur Beantwortung solcher Fragen haben sich Beweissysteme als nützlich erwiesen. Es handelt sich hierbei um mathematische Formalismen, die (in einem abstrakten Sinn) die Beweise genau jener Aussagen erzeugen können, welche Konsequenzen der Logik sind. Gerhard Gentzen entwarf im Jahr 1935 für mehrere bedeutende Logiken ein elegantes Beweissystem namens "Sequenzenkalkül", welches sich durch die Eigenschaft der "Analytizität" auszeichnet. Vereinfacht gesagt bedeutet Analytizität, dass sich der Beweis einer komplexen Aussage stets aus den Beweisen einfacherer Aussagen zusammenfügen lässt. Auf diese Weise wird die Komplexität einer Aussage mit der Struktur ihres Beweises in Bezug gesetzt. Leider ist es für die meisten interessanten Logiken schwierig oder sogar unmöglich, einen Sequenzenkalkül mit der Analytizitätseigenschaft zu konstruieren. Aus diesem Grund hat man sich in letzter Zeit zumeist auf die Entwicklung komplizierter neuer Beweissysteme konzentriert, die den Sequenzenkalkül ersetzen. Dies hat allerdings seinen Preis: Ungeachtet der Analytizitätseigenschaft dieser Beweissysteme eignen sie sich aufgrund ihrer Komplexität nur bedingt zur Untersuchung logischer Fragen. Im vorliegenden Projekt soll untersucht werden, wie man komplizierte Beweissysteme mit der Analytizitätseigenschaft auf Sequenzenkalküle zurückführen kann. Die so erhaltenen Sequenzenkalküle werden verschiedene Eigenschaften haben, die zwar schwächer als Analytizität, aber dennoch nützlich sind. Solche Beweissysteme werden "beschränkte Sequenzenkalküle" genannt. Das Projekt wird den Grundstein für die Erforschung beschränkter Sequenzenkalküle legen und sie zum Studium logischer Fragen verwenden. Schlussendlich werden wir untersuchen, inwiefern beschränkte Sequenzenkalküle als einheitlicher mathematischer Formalismus für die Konstruktion von Beweissystemen und die Untersuchung von Logiken dienen können.

Dieses Projekt entwickelte eine neue und einfachere Methode zur Analyse komplexer Schlussfolgerungssysteme, wie sie in der Informatik und verwandten Fachgebieten verwendet werden. Die wichtigsten Ergebnisse lassen sich in drei Punkten zusammenfassen: Es führte einen einheitlichen Beweisrahmen für viele verschiedene Logiken ein, erzielte neue Resultate darüber, wie schwierig diese Schlussfolgerungsprobleme sind, und stellte erste Werkzeuge zur Automatisierung solcher Schlussfolgerungen bereit. Das Projekt zeigte, dass viele nicht-klassische Logiken - die beispielsweise verwendet werden, um Schlussfolgerungen über Ressourcen wie Zeit, Speicher oder Information zu modellieren - innerhalb eines einzigen, einfacheren Rahmens untersucht werden können. Anstatt für jede Logik eine eigene spezialisierte Methode zu entwickeln, wurde gezeigt, dass es möglich ist, die standardisierte und gut verstandene Methode, den Sequenzenkalkül, zu nutzen und nur sorgfältig kontrollierte zusätzliche Schritte zuzulassen. Diese neuen Systeme wurden als beschränkte Sequenzenkalküle bezeichnet. Eine zentrale Innovation bestand darin, die Behandlung dieser zusätzlichen Schritte neu zu denken. Traditionell wurde versucht, sie vollständig zu eliminieren, was jedoch bei vielen wichtigen Logiken nicht möglich ist. Das Projekt zeigte stattdessen, dass die Zulassung solcher Schritte in eingeschränkter Form einen Großteil der Nützlichkeit des Systems bewahrt und zugleich seine Anwendbarkeit erheblich erweitert. Dadurch wurde es möglich, innerhalb eines einheitlichen Rahmens die wesentlichen Einsichten vieler zuvor entwickelter, komplexerer Methoden zurückzugewinnen. Damit wurde ein seit Langem bestehendes Problem des Fachgebiets aufgegriffen: die Vielzahl sich überschneidender und schwer vergleichbarer Beweissysteme. Der neue Ansatz bietet eine gemeinsame Grundlage für ihr Verständnis und ihren Vergleich. Ein weiteres zentrales Ergebnis war die Entwicklung neuer Methoden zur Analyse der Schwierigkeit von Schlussfolgerungen in diesen Systemen. Das Projekt führte Techniken auf der Grundlage von Wohlquasiordnungen ein, die sicherstellen, dass bestimmte rechnerische Prozesse zwangsläufig terminieren. Mithilfe dieser Methoden wurden neue Resultate dazu erzielt, ob Schlussfolgerungsprobleme überhaupt lösbar sind (Entscheidbarkeit) und wie komplex sie sind. Ein bemerkenswertes Beispiel ist die grundlegende Fuzzy-Logik MTL, für die erstmals eine aussagekräftige obere Schranke für ihre Komplexität bestimmt wurde; damit wurde ein langjähriges offenes Problem gelöst. Gegen Ende des Projekts wurde diese Schranke noch einmal deutlich verbessert. Darüber hinaus untersuchte das Projekt auch praktische Aspekte, indem es eine prototypische Implementierung dieser Methoden als automatisierte Beweiswerkzeuge entwickelte. Solche Werkzeuge sind wichtig für Anwendungen wie die Verifikation von Software, bei der überprüft werden muss, ob Systeme korrekt funktionieren. Schließlich erweiterte das Projekt den klassischen Algorithmus aus den 1930er Jahren zur Eliminierung von Schnittregeln aus Sequenzenkalkülen auf diesen neuen Kontext. Dies gelang für mehrere wichtige Fälle, während die allgemeine Theorie die Grundlage für weitere laufende Arbeiten bildet. Insgesamt liefert das Projekt ein einheitliches Verständnis komplexer Schlussfolgerungssysteme, mit neuen Ergebnissen zu ihrer rechnerischen Komplexität und Fortschritten in Richtung automatisierter Beweisführung.