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.

News

  • Stella Mahler will give a talk on Herbrand’s theorem for inductive proofs at the Proof Society Meeting in Birmingham, September 1 – 13, 2024.
  • Stella Mahler will give a talk on Herbrand’s theorem for inductive proofs at the Logic Colloquium 2024 in Gothenburg, Sweden, June 25.
  • Our paper Herbrand’s Theorem in Inductive Proofs (Alexander Leitsch and Anela Lolic) got accepted for publication at LPAR 2024!
  • Our paper On Proof Schemata and Primitive Recursive Arithmetic (Alexander Leitsch, Anela Lolic, and Stella Mahler) got accepted for publication at LPAR 2024 Complementary Volume!
  • Our preprint Herbrand’s Theorem in Refutation Schemata (Alexander Leitsch and Anela Lolic) is available on arXiv.
  • Alexander Leitsch gave a talk on First-Order Schemata and Herbrand’s theorem at the TU Wien Computational Logic Seminar, May 22, 2024.

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

Project Members