Structure and Expressivity: The Mathematical Foundations of Inductive Reasoning

Induction is a reasoning principle of fundamental importance in a large number of fields.
Many areas of mathematics would not be thinkable without inductive proofs. In computer science, induction is indispensable for reasoning about programs and data structures. However, the problem of the automation of proof by induction - while crucial for software verification - is far from being resolved in a satisfactory way.

In proof theory, a branch of mathematical logic, one investigates proofs as mathematical objects per se. This project is concerned with the proof-theoretic analysis of inductive proofs.
Its aim is to develop a radically new approach to the automation of proof by induction based on a mathematical investigation of the combinatorial structure of formal proofs.
One approach we intend to pursue to that aim is to characterize provability in inductive theories in terms of formal language theory.