Algorithmic introduction of 2-cuts / von Michael Peter Lettmann
Weitere Titel
Algorithmic Introduction of 2-cuts
Verfasser / Verfasserin Lettmann, Michael Peter
Begutachter / BegutachterinLeitsch, Alexander ; Baaz, Matthias
ErschienenWien, 2018
Umfangxvii, 159 Seiten : Illustrationen
HochschulschriftTechnische Universität Wien, Dissertation, 2018
Zusammenfassung in deutscher Sprache
Schlagwörter (EN)Lemma generation / proof theory / automated deduction / proof grammar / sequent calculus
URNurn:nbn:at:at-ubtuw:1-117602 Persistent Identifier (URN)
 Das Werk ist frei verfügbar
Algorithmic introduction of 2-cuts [1.78 mb]
Zusammenfassung (Englisch)

One of the crucial results in proof theory is Gentzens Hauptsatz, also known as the cut-elimination theorem. Cut-elimination is a technique to incorporate only the necessary content of lemmas within a formal proof into the proof while eliminating the additional structure of the lemma. The resulting object, a cut-free proof, gives insights about the computational content of a proof and is of major interest for subjects such as proof mining and automated theorem proving. Such proofs show an analytic behaviour mainly discernible in the subformula property which tells us that within the proof only subformulas of the statement are used. A drawback is the large size of cut-free proofs, due to missing structure expressible by lemmas. In this thesis, we propose an inversion of the cut-elimination method based on a connection of formal grammars and proof theory. We specify characteristic grammars for cut formulas according to the arithmetical hierarchy up to 2 formulas and discuss whether the existence of such a grammar allows us to rewrite a given cut-free proof, now with 2-cut formulas, in order to reduce the proof size. Thereby, we revisit 1-cut introduction, present an algorithm to introduce 2 cuts which is shown to be complete for a fragment, and discuss the decidability of the problem whether 2 cuts exist for a given grammar. Moreover, we show that our method of 2-cut introduction achieves an exponential compression of the proof size.

Das PDF-Dokument wurde 15 mal heruntergeladen.