A general analysis of cut-elimination by CERes

Abstract

Das Prinzip der Beweiskompositionalit¨at wird durch die Inferenzregel Schnitt formal vertreten. Beweise einfacher Lemmas k¨onnen durch die Schnittregel zusammengesetzt werden, um damit komplexe Theoremen beweisen zu k¨onnen. Gentzens Hauptsatz, in welchem die Eliminierbarkeit der Schnittregel bewiesen wird, ist einer der wichtigsten und ber ¨uhmtesten S¨atze der Beweistheorie, denn viele n¨utzliche Korollare, wie zum Beispiel Herbrands Satz und die Teilformeleigenschaft, folgen aus ihm. Um einige von diesen Korollaren in der Praxis benutzen zu k¨onnen, muss man zuerst Algorithmen entwickeln, welche die Schnittinferenzen aus Beweisen wirklich eliminiert. Die Methode CERes zeichnet sich dabei als eine effiziente und robuste Methode f ¨ur Schnittelimination aus.<br />Diese Dissertation enth¨alt eine generelle Untersuchung von CERes durch die Entwicklung vieler verschiedenen Varianten, die in zwei Gruppen eingeteilt werden k¨onnen. Varianten der ersten Gruppe sind charakterisiert durch ¨Anderungen in der Konstruktion der schnittzugeh¨origen Klausenmenge und der Projektionen. Sie nutzen die M¨oglichkeit aus, Inferenzen zu permutieren, und benutzen strukturelle Klauselformtransformationen, um die exponentielle Vergr ¨oßerung der Klausenmenge zu vermeiden. Die zweite Gruppe enth¨alt Verfeinerungen des Resolutionskalk ¨uls zum Zwecke der Schnittelimination durch CERes. Die Verfeinerungen beschr¨anken die Benutzung der Inferenzregeln des Resolutionskalk ¨uls, sodass sich die Varianten in der Mitte, bez ¨uglich kanonischer Refutationen, zwischen unbeschr¨anktem CERes und reduktiven Schnitteliminationsmethoden bewegen. Deswegen k¨onnen diese Varianten weiter erkl¨aren, wodurch diese zwei anscheinend sehr verschiedenen Methoden sich wirklich unterscheiden und trotzdem ¨ahnlich sind.<br />Schließlich wird in dieser Dissertation auch gezeigt, wie CERes in eine Methode f ¨ur die Einf ¨urung atomarer Schnitte (CIRes) umgewandelt werden kann. Diese Methode kann Beweise komprimieren, und es wird vermutet, dass exponentiell kleinere Beweise dadurch erhalten werden k¨onnen.<br />

The cut rule formally represents the principle of compositionality of proofs. Proofs of simple lemmas can be composed using the cut rule to form proofs of more complex theorems. The cut-elimination theorem (i.e. the completeness of Sequent Calculus without the cut-rule) is one of themost important and famous theorems of proof theory, mainly because it leads to many useful corollaries, such as the subformula property and the midsequent or Herbrand's theorem. However, in order to exploit these corollaries in practice, it is often necessary to have algorithms for the actual elimination of cuts, and CERes stands out as an efficient and robust cut-elimination method based on the resolution calculus.<br />This thesis contains a general investigation of CERes through the development of several variants of the method, which can be distinguished in two groups. The first group consists of variants obtained by modifying the construction of cut-pertinent clause sets and projections. They exploit the possibility of swapping inferences in sequent calculus proofs and use structural clause form transformation to avoid the exponential blow-up in the size of the clause sets. The second group consists of refinements of the resolution calculus that are specific for cut-elimination by CERes. A few refinements are defined by increasingly restricting the applicability of the inference rules of the resolution calculus in such away that the variants are intermediary, regarding simulation with respect to canonic refutations, between the unrestricted CERes and reductive methods of cut-elimination (i.e. methods based on local proof rewriting rules).<br />Consequently, this group of variants further clarifies the differences and similarities between these two kinds of methods, which appear to be so distinct from each other.<br />Furthermore, this thesis shows how CERes can be transformed into a method of atomic-cut-introduction (CIRes), which is capable of compressing proofs. Asymptotically, an exponential compression in the size of proofs is conjectured to be achievable by the method.