Advances in schematic cut elimination

Abstract

In dieser Dissertation untersuchen wir Formel- und Beweisschemata in der Aussagen- und in der Prädikatenlogik. Mit -schematischmmeinen wir dass Formeln und Beweise durch einen freien numerischen Parameter indiziert sind. Im propositionalen Fall untersuchen wir eine Erweiterung eines Entscheidungsverfahrens für die Erfüllbarkeit regulärer aussagenlogischer Formelschemata (definiert in [4]) auf mehrere freie Parameter. Der Hauptteil der Arbeit besteht in der Untersuchung von Schnittelimination in prädikatenlogischen Beweisschemata mit Hilfe der CERES-Methode für Beweisschemata defininiert in [31]. Diese Beweisschemata haben eine zyklische Form mit einem freien numerischen Parameter. Die Schnitteliminationsmethode CERES definiert in [14] extrahiert eine sogenannte charakteristische Klauselmenge aus einem Beweis im Sequentialkalkül und widerlegt diese mit Resolution. Die charakteristische Klauselmenge repräsentiert die Schnittstruktur des Beweises und ist immer unerfüllbar. Im Gegensatz zur Methode in [14] welche eine vollständige Schnitteliminationsmethode für die Logik erster Stufe liefert ist die Methode in [31] inhärent unvollständig. Das Hauptproblem besteht darin dass Beweischemata unendliche Folgen von Beweis-Schemata repräsentieren und viele theoretische Resultate in [14] nicht für Schemata gelten. Insbesondere ist auch unklar wie und ob eine reduktive Schnittelimination für Schemata definiert werden kann. Auch die schematische Resolution ist nicht mehr vollständig für unerfüllbare Klausel-Schemata. Das Problem der Spezifikation schematischer Resolutionsbeweise zur Widerlegung der schematischen charakteristischen Klauselmengen nimmt einen zentralen Platz in der Untersuchung ein. Da es dazu keinen theoretischen Hintergrund gibt untersuchen wir das Problem anhand typischer Fallstudien der Beweistheorie (wie das unendliche Schubfachprinzip). An Hand dieser Fallstudien untersuchen wir die Expressivität des Formalismus in [31] und zeigen seine Grenzen auf. Im Zuge dieser Untersuchung verallgemeinern wir den schematischen Resolutionskalkül und entwickeln eine Methode der Herbrand-Extraktion (welche aber relativ eng auf spezifische Schemata beschränkt ist). Abschließend ist zu sagen, dass automatische Beweiser in der Auffindung der Resolutions-Widerlegungs-Schemata eine wichtige Rolle gespielt haben und geben einen Hinweis auf potentielle künftige Verwendung von automatischen Beweisern. vii

Abstract In this dissertation we study schematic formulae and proofs from both the propositional and first-order perspective. By schematic we mean that the formulae have a free numeric parameter indexing the formulae. In the propositional case we study an extension of a decision procedure for satisfiability of regular propositional schematic formulae, defined in [4], allowing for multiple free parameters within a single formula. Our work concerning first-order schematic formulae makes up the major of the dissertation and is mainly concerned with cut-elimination for proof schemata using the CERES method [31]. By proof schemata, we are referring to a restricted form of cyclic proofs with a free indexing parameter. The CERES method of cut elimination introduced in [14] extracts what is referred to as the characteristic clause set from a sequent calculus proof and uses resolution to refute the clause set. The characteristic clause set represents the cut structure of the sequent calculus proof it is derived from and is always unsatisfiable. Unlike the work of [14], which introduces a complete method for cut elimination in first order logic, [31] only introduces a framework which can be used to define proof schemata and possibly eliminate the cuts within a given proof schemata. The problem with proof schemata is that they essentially define an infinite sequence of proofs and many theoretic results used in [14] no longer hold for proof schemata. For example, reductive cut elimination is not as straight forward as it was for first-order sequent calculus proofs and it is unclear if it is even possible to define a reductive method for proof schemata. Also, most importantly, resolution is on longer a complete method for unsatisfiable clause sets, specifically, it is not complete for unsatisfiable schematic clause sets. This issue with resolution being one of the main issues addressed in this thesis. We approach this problem of the lack of a theoretic backbone for cut-elimination on proof schemata by constructing several formal proofs in a schematic version of the standard sequent calculus, each of which is based on a well studied problem (the infinitary pigeonhole principle) often used in the analysis of proof complexity within a given proof system. Using these formal proofs, we apply the schematic version of the CERES method to each of the proofs to see if the method is expressive enough to handle cut elimination for the given proof schema, and if it is not, we ask if we can generalize certain parts of the method to handle the given proof schema and allow for cut elimination in this more general framework. In the process, we develop a generalized version of the resolution calculus introduced in [31], a possible method for Herbrand sequent extraction, though the method is quite restrictive and relies a lot on the structure of the proof schema, and combinatorial results pertaining to the structure of the characteristic clause sets of the given proof schemata. As a final remark, theorem provers where heavily used in the application of the schematic CERES method to the formalized proof schemata used in this dissertation. We also provide an outline as to how this was done and what results where attained with the aid of automated theorem provers, as well as, idea on how automated theorem provers might be beneficial to future research in this subject.