Applications of higher-order cut-elimination

Abstract

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ürstenberg’s 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.