Characteristic clause sets and proof transformations

Abstract

Die Beweistheorie jener Zweig der mathematischen Logik, in dem mathematisches Schließen und mathematische Beweise untersucht werden.<br />Sie entstand aus Hilberts Programm: der Suche nach Konsistenzbeweisen für formale Theorien. In den 1950ern begann sich der Fokus der Beweistheorie auf Anwendungen formaler Methoden auf konkrete Beweise zu verschieben.<br />Die Methode CERES (cut-elimination by resolution) verwendet Techniken des automatischen Beweisens zur Automatisierung der Schnittelimination.<br />Der beweistheoretische Kern dieser Methode ist die Extraktion einer charakteristischen Klauselmenge aus einem Beweis. Eine Resolutionswiderlegung dieser Klauselmenge dient als Skelett eines schnittfreien Beweises.<br />Die vorliegende Dissertation ist eine Untersuchung des Potentials dieser Art von Klauselmengen zur Charakterisierung des mathematischen Inhaltes und der Struktur eines formalen Beweises. Es wird eine Variante dieser Klauselmengen vorgestellt, das Profil, welches die folgenden Vorteile gegenüber der originalen charakteristischen Klauselmenge bietet:<br />Es erzeugt niemals längere Beweise, sondern ist besser in der Behandlung von Redundanzen, was eine nicht-elementare Beschleunigung ermöglicht.<br />Außerdem hat es die angenehme theoretische Eigenschaft invariant unter Regelpermutationen zu sein. Daraus folgt sofort, dass zwei Beweise mit dem gleichen Beweisnetz auch das gleiche Profil haben.<br />In dieser Arbeit wird eine große Klasse von Beweistransformationen definiert, die das Profil nicht verändern. Als Basis dieses Resultats wird zuvor eine detaillierte Analyse des Verhaltens des Profils unter der Schnittelimination durchgeführt, die zu einem sehr natürlichen Resultat führt.<br />Es wird gezeigt werden, dass das Profil in einer sehr engen Beziehung zu Herbrand-Disjunktionen steht: Das Profil besteht aus zwei Teilen die genau zu redundanzfreien Varianten der beiden partiellen Herbrand-Disjunktionen eines Beweises mit Schnitten korrespondieren.<br />In einer Fallstudie werden zwei unterschiedliche Beweise eines mathematisches Theorems mit Hilfe von charakteristischen Klauselmengen analysiert, um das Anwendungspotential zu illustrieren.<br />

Proof Theory is the branch of mathematical logic that investigates mathematical reasoning and mathematical proofs. This area emanated from Hilbert's Program calling for consistency proofs of formal theories. In the 1950s the focus of proof theory began shifting towards applications of formal methods to concrete proofs in order to obtain new mathematical results.<br />The method CERES (cut-elimination by resolution) uses techniques from automated theorem proving for the automation of cut-elimination. The main proof-theoretical tool of this method is the extraction of a characteristic clause set from a proof, a resolution refutation of which serves as the skeleton of a cut-free proof.<br />This thesis is an investigation of the potential of these kind of clause sets for characterizing the mathematical content and structure of a formal proof. We first define a variant of these clause sets, the profile that has several advantages w.r.t. the original characteristic clause sets:<br />It is computationally superior in the sense that it will never generate longer proofs with CERES, but is better in detecting certain redundancies thus allowing even a non-elementary speed-up. Furthermore, it has the nice theoretical property of being invariant under rule permutations which shows that two proofs having the same proof net will also have the same profile.<br />We will isolate a large class of proof transformations and show that they leave the profile invariant. As a basis for this result we will give a detailed analysis of the behavior of the profile under cut-elimination whose result will be particularly natural.<br />We will show that the profile is intimately related to Herbrand-disjunctions. It turns out that the profile has two dual parts corresponding to pruned versions of the two partial Herbrand-disjunctions that can be extracted from a proof with cuts: One being the instances of the end-sequent and one the instances of the cut-formulas.<br />Finally we will perform a case study where two different proofs of a simple mathematical theorem are analyzed by characteristic clause sets in order to demonstrate its potential for applications.