In proof theory, proofs are considered as objects. Formal proof analysis deals with
computational transformations of these objects in order to analyze proofs. For instance, we
might be interested in the essence of a proof, which can be gained by extracting information
from the proof, based on the so-called Herbrands Theorem. By extracting this information
from a formal proof of a statement, we might obtain important information about the variables
occurring in the statement, or their upper and lower bounds.
Mathematical induction is one of the essential concepts in the mathematician`s toolbox.
Though, its use makes formal proof analysis difficult. In essence, induction compresses an
infinite argument into a finite statement. This process obfuscates information essential for
computational proof transformation and automated reasoning. Herbrands theorem covers
classical predicate logic. While there are interpretations of Herbrands theorem extending its
scope to induction, these results are at the expense of analyticity, the most desirable property
of Herbrands Theorem used for extracting important information from the proofs. Given the
rising importance of formal mathematics and inductive theorem proving to many areas of
computer science, developing our understanding of the analyticity boundary is essential.
In this proposal we tackle these issues using a relatively novel formulation of induction as
sequences of proofs, referred to as proof schemata. This type of cyclic representation has been
gaining traction the past few years and will in all likelihood play an integral role in automated
theorem proving and proof theory in years to come. However, unlike other approaches to
cyclic proof theory, we focus on the extraction of a finite representation of the information
contained in formal proofs. Development of a computational proof theoretic method for the
extraction of this information for expressive inductive theories is our main objective.