Anwendungen der Schnittelimination hoeherer Stufe / von Martin Riener
Weitere Titel
Applications of Higher-Order Cut-Elimination
VerfasserRiener, Martin
Begutachter / BegutachterinLeitsch, Alexander
ErschienenWien, 2017
Umfang169 Seiten
HochschulschriftTechnische Universität Wien, Dissertation, 2017
Arbeit an der Bibliothek noch nicht eingelangt - Daten nicht geprueft
Abweichender Titel nach Übersetzung der Verfasserin/des Verfassers
Schlagwörter (DE)Beweistheorie / Automatische Deduktion
Schlagwörter (EN)proof theory / automated deduction
URNurn:nbn:at:at-ubtuw:1-102927 Persistent Identifier (URN)
 Das Werk ist frei verfügbar
Anwendungen der Schnittelimination hoeherer Stufe [7.03 mb]
Zusammenfassung (Englisch)

The method of Cut-Elimination by Resolution (CERES) bridges the fields of proof theory and automated theorem proving. Its proof theoretic value lies in the extraction of information from a theorem beyond its mere truth while its contribution to the automated theorem proving community lies in the generation of hard problems for which, at least in theory, a proof can always be found. An example for such a successful analysis in first-order logic was the formalization of Fürstenbergs proof of the infinity of primes. So far, CERES!, the extension of CERES to higher-order logic was missing an application of equivalent complexity. This thesis develops the CERES! method further, improving the interplay with automated higher-order theorem provers. Furthermore we explore the use of expansion proofs as a concise representation of witness terms for weak quantifiers, the essential information generated by CERES. Moreover, we introduce CERES! =, a variant which targets the fragment of functional quantification with first-order equality and definition rules. Finally, we introduce LLK, a LATEX inspired proof input language and Sunburst trees, a global visualization of sequent calculus proofs and the implementation of these proof analysis techniques in the GAPT system. As a case study, we formalize the infinite pigeon hole principle and extract functions enumerating arbitrary many pigeons in the infinite-sized hole. We compare our results to those of Ratiu and Trifonov which were found via A-translation and modified Realizability. Simultaneously, we explore the gradient of solvable problems for higher-order provers, identifying possible directions for future development.