PANDAFOREST

Proof analysis and automated deduction for recursive structures is a joint international project between Austria (funded by FWF, PI Anela Lolić) and Czechia (funded by GAČR, PI David M. Cerna) with a focus on computational proof theory and automated reasoning.

  • Name: Proof analysis and automated deduction for recursive structures.
  • FWF project number: I 5848.
  • Project timeline: Sept. 2022 – Aug 2025.

Description

Mathematical induction is one of the essential concepts in the mathematician’s toolbox. Though, it has proven itself difficult to handle formally.  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 the classical setting where this information can be finitely represented and used to analyze proofs and provide a formal foundation for automated theorem proving. While there are interpretations of Herbrand’s theorem extending its scope to formal number theory, these results are at the expense of analyticity, the most desirable property of Herbrand’s theorem.  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 project we tackle these issues using a relatively novel formulation of induction as sequences of proofs, referred to as proof schemata. Proof schemata allow a recursive finite representation of many proof theoretically interesting objects as well as proof structures studied by the automated theorem proving community. Additionally, proof schemata provide the perfect framework to discuss proof analytic completeness of the method we plan to develop. 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 Herbrand information contained in formal proofs. Development of a computational proof theoretic method for the extraction of Herbrand information for expressive inductive theories is our main objective. Furthermore, we hypothesize that developments in the proof theory of induction, using our chosen methodology (CERES style proof analysis), will lead to the development of more powerful inductive theorem provers.

Collaborators

Team Members