Analysis of Clause set Schema Aided by Automated Theorem Proving: A Case Study [Extended Paper]

TL;DR

This paper explores the use of automated theorem proving in analyzing proof schemata, specifically applying the schematic CERES method to a formalized version of the infinitary pigeonhole principle, highlighting its capabilities and limitations.

Contribution

It formalizes a schematic version of the NiA-schema in the LKS-calculus and applies the schematic CERES method for proof analysis, marking a novel application to a mathematical argument.

Findings

First application of schematic CERES to a mathematical argument

Discussion of ATP's role and limitations in schematic proof analysis

Identification of expressive power issues in schematic resolution calculus

Abstract

The schematic CERES method [8] is a recently developed method of cut elimination for proof schemata, that is a sequence of proofs with a recursive construction. Proof schemata can be thought of as a way to circumvent adding an induction rule to the LK-calculus. In this work, we formalize a schematic version of the infinitary pigeonhole principle, which we call the Non-injectivity Assertion schema (NiA-schema), in the LKS-calculus [8], and analyse the clause set schema extracted from the NiA-schema using some of the structure provided by the schematic CERES method. To the best of our knowledge, this is the first appli- cation of the constructs built for proof analysis of proof schemata to a mathematical argument since its publication. We discuss the role of Automated Theorem Proving (ATP) in schematic proof analysis, as well as the shortcomings of the schematic CERES method concerning the formalization of the NiA-schema, namely, the expressive power of the schematic resolution calculus. We conclude with a discussion concerning the usage of ATP in schematic proof analysis.