Automation of cut-elimination in proof schemata

Abstract

Die Schnittelimination von Gentzen ist eine der bekanntesten Methoden zur Beweistransformation, die eine grundlagende Rolle in der automatischen Analyse mathematischer Beweise spielt. In einem Beweis haben die Schnittformeln die Bedeutung der Lemmata. Ein Beweis ohne die Schnittformulas entspricht der Elimination der Lemmata. Man sagt, dass ein Beweis ohne Lemmata eigentlich ein analytischer Beweis ist, wenn alle Formeln des Beweises kommen in Endsequent vor.<br /> Eine Verbesserung der Methode von Gentzen ist die Methode CERES (Schnittelimination durch Resolution). Die ist eine Methode fuer Schnittelimination in der Logik erster Stufe, die die Teile des Beweises mit Schnittregeln analysiert. Diese Information ist besonderes wertvoll fuer das Bauen einer Menge von Klauseln, die immer unerfuellbar ist. Die Widerlegung der Klausemenge hat einige Beschraenkungen von theoretische und praktische Natur. Man kann zum Beispeil CERES nicht anwenden wenn der Beweis ein Induktionsregel beinhaltet.<br /> Ausserdem, wenn das Beweis zu gross ist, ist die Widerlegung der Klausemenge nicht moeglich, weil auch die besten automatischen Theorembeweisern (wie Prover9 und Vampire) keine Loesung finden. Eine Loesung des ersten Problems ist durch die Erweiterung von CERES auf CERESs gegeben. Die Methode CERESs ist eine Methode fuer Schnittelimination in den Schemata erster Stufe. Schemata dienen dazu, unendliche Folgen von Beweisen darzustellen; diese Schemata bezeichnen wir als Beweisschemata. Dennoch, die Methode CERESs ist nicht ganz automatisierbar, weil das Problem des Findens eine Resolutionwiderlegung einer Menge von schematischen Klauseln erster Stufe nicht entscheidbar ist.<br /> In dieser Dissertation beschreiben wir die Methode CERESs und praesentieren die Algorithmen und Werkzeuge des GAPT-Systems fuer automatische Analyse schematischer Beweise erster Stufe.<br />

Cut-elimination introduced by Gentzen is the most prominent form of proof transformation in logic and plays a key role in automating the analysis of mathematical proofs. The removal of cuts corresponds to the elimination of intermediate statements (lemmas) used in proofs. The result is a proof which is analytic in the sense that all statements in the proof are subformulas of the result. An improvement of the Gentzen's method is the method CERES (Cut Elimination by Resolution).<br /> It is a method of cut-elimination in first-order logic which analyzes the parts of the proof used in cut inferences. This information is used to construct a set of clauses which is always unsatisfiable. The refutation of this clause-set serves as a skeleton of a proof with at most atomic cuts. The method CERES has some limitations from a theoretical and practical point of view.<br /> For example, CERES is not applicable in the presence of induction.<br />Furthermore, for large proofs the clause-sets cannot be refuted because automated theorem provers (such as Prover9) fail. A solution for the first problem is obtained by extending CERES to CERESs - a method for cut-elimination in first-order schema. The concept of schemata allows us to represent an infinite sequence of proofs as a singe object called proof schemata. Nevertheless, the whole process is not fully automatable, because the problem of finding a resolution refutation for the set of first-order claus schemata is not semi-decidable.<br /> In this thesis we describe the method CERESs and present algorithms and tools which are used by the GAPT framework for (semi)automated analysis of first-order proofs and proof schemata.