Proof analysis AND Automated deduction FOr REcursive STructures (PANDAFOREST)

PANDAFOREST is a joint inter- national project between the Czech Academy of Science Institute of Computer Science (CAS ICS) (PI: David M. Cerna) and The Technical university of Vienna (TUV) (PI: Anela Lolic) funded by GAČR and FWF with a focused on com- putational proof theory and auto- mated reasoning.

Project timeline: July 2022 - June 20 2025

Collaborators:
Stefan Hetzl (TUV)
Nicolas Peltier (CNRS, LIG)
Daniele Nantes-Sobrinho (UnB)
Reuben Rowe (Royal Holloway)

Team Members:

Description:
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 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.
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 frame work to discuss proof analytic completeness of the method we plan to develop. This type of cyclic representation has been gaining traction the pass 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.

Results and Publications: