Bibliographic Metadata

Title
A general analysis of cut-elimination by CERes / Bruno Woltzenlogel Paleo
AuthorWoltzenlogel Paleo, Bruno In der Gemeinsamen Normdatei der DNB nachschlagen
CensorLeitsch, Alexander ; Baaz, Matthias
Published2009
DescriptionIII, 234 S.
Institutional NoteWien, Techn. Univ., Diss., 2009
Annotation
Zsfassung in dt. Sprache
LanguageEnglish
Bibl. ReferenceOeBB
Document typeDissertation (PhD)
Keywords (DE)Logik / Schnittelimination / Automatisches Beweisen / Beweistheorie
Keywords (EN)Logic / Cut-Elimination / Automated Deduction / Proof Theory
Keywords (GND)Beweistheorie / Automatisches Beweisverfahren / Schnittelimination
URNurn:nbn:at:at-ubtuw:1-32321 Persistent Identifier (URN)
Restriction-Information
 The work is publicly available
Files
A general analysis of cut-elimination by CERes [1.38 mb]
Links
Reference
Classification
Abstract (German)

Das Prinzip der Beweiskompositionalitat wird durch die Inferenzregel Schnitt formal vertreten. Beweise einfacher Lemmas konnen durch die Schnittregel zusammengesetzt werden, um damit komplexe Theoremen beweisen zu konnen. Gentzens Hauptsatz, in welchem die Eliminierbarkeit der Schnittregel bewiesen wird, ist einer der wichtigsten und ber uhmtesten Satze der Beweistheorie, denn viele nutzliche Korollare, wie zum Beispiel Herbrands Satz und die Teilformeleigenschaft, folgen aus ihm. Um einige von diesen Korollaren in der Praxis benutzen zu konnen, 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.

Diese Dissertation enthalt eine generelle Untersuchung von CERes durch die Entwicklung vieler verschiedenen Varianten, die in zwei Gruppen eingeteilt werden konnen. Varianten der ersten Gruppe sind charakterisiert durch Anderungen in der Konstruktion der schnittzugehorigen Klausenmenge und der Projektionen. Sie nutzen die Moglichkeit aus, Inferenzen zu permutieren, und benutzen strukturelle Klauselformtransformationen, um die exponentielle Vergr oßerung der Klausenmenge zu vermeiden. Die zweite Gruppe enthalt Verfeinerungen des Resolutionskalk uls zum Zwecke der Schnittelimination durch CERes. Die Verfeinerungen beschranken die Benutzung der Inferenzregeln des Resolutionskalk uls, sodass sich die Varianten in der Mitte, bez uglich kanonischer Refutationen, zwischen unbeschranktem CERes und reduktiven Schnitteliminationsmethoden bewegen. Deswegen konnen diese Varianten weiter erklaren, wodurch diese zwei anscheinend sehr verschiedenen Methoden sich wirklich unterscheiden und trotzdem ahnlich sind.

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 konnen.

Abstract (English)

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.

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).

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.

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.