<div class="csl-bib-body">
<div class="csl-entry">Lettmann, M. P. (2018). <i>Algorithmic introduction of π2-cuts</i> [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2018.60480</div>
</div>
-
dc.identifier.uri
https://doi.org/10.34726/hss.2018.60480
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/7308
-
dc.description.abstract
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.
en
dc.language
English
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
Lemma generation
en
dc.subject
proof theory
en
dc.subject
automated deduction
en
dc.subject
proof grammar
en
dc.subject
sequent calculus
en
dc.title
Algorithmic introduction of π2-cuts
en
dc.title.alternative
Algorithmic Introduction of π2-cuts
de
dc.type
Thesis
en
dc.type
Hochschulschrift
de
dc.rights.license
In Copyright
en
dc.rights.license
Urheberrechtsschutz
de
dc.identifier.doi
10.34726/hss.2018.60480
-
dc.contributor.affiliation
TU Wien, Österreich
-
dc.rights.holder
Michael Peter Lettmann
-
dc.publisher.place
Wien
-
tuw.version
vor
-
tuw.thesisinformation
Technische Universität Wien
-
dc.contributor.assistant
Baaz, Matthias
-
tuw.publication.orgunit
E192 - Institut für Logic and Computation
-
dc.type.qualificationlevel
Doctoral
-
dc.identifier.libraryid
AC15203741
-
dc.description.numberOfPages
159
-
dc.identifier.urn
urn:nbn:at:at-ubtuw:1-117602
-
dc.thesistype
Dissertation
de
dc.thesistype
Dissertation
en
dc.rights.identifier
In Copyright
en
dc.rights.identifier
Urheberrechtsschutz
de
tuw.advisor.staffStatus
staff
-
tuw.assistant.staffStatus
staff
-
item.fulltext
with Fulltext
-
item.cerifentitytype
Publications
-
item.mimetype
application/pdf
-
item.openairecristype
http://purl.org/coar/resource_type/c_db06
-
item.languageiso639-1
en
-
item.openaccessfulltext
Open Access
-
item.openairetype
doctoral thesis
-
item.grantfulltext
open
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering