Bibliographic Metadata

Title
Applications of higher-order cut-elimination / by Martin Riener
Additional Titles
Anwendungen der Schnittelimination höherer Stufe
AuthorRiener, Martin
CensorLeitsch, Alexander
PublishedWien, 2017
Descriptionxi, 169 Seiten : Illustrationen
Institutional NoteTechnische Universität Wien, Dissertation, 2017
Annotation
Zusammenfassung in deutscher Sprache
Annotation
Abweichender Titel nach Übersetzung der Verfasserin/des Verfassers
LanguageEnglish
Bibl. ReferenceOeBB
Document typeDissertation (PhD)
Keywords (DE)Beweistheorie / Automatische Deduktion
Keywords (EN)proof theory / automated deduction
Keywords (GND)Beweistheorie / Automatisches Beweisverfahren / Schnittelimination / Prädikatenlogik / Stufe n
URNurn:nbn:at:at-ubtuw:1-102927 Persistent Identifier (URN)
Restriction-Information
 The work is publicly available
Files
Applications of higher-order cut-elimination [7.03 mb]
Links
Reference
Classification
Abstract (English)

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.

Stats
The PDF-Document has been downloaded 22 times.