Proof analysis and autom. deduction for recursive structures

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.

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 Herbrand's 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. Herbrand's theorem covers classical predicate logic. While there are interpretations of Herbrand's theorem extending its scope to induction, these results are at the expense of analyticity, the most desirable property of Herbrand's 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.