**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**:

Cerna, D. M. **Recursive First-order Syntactic Unification Modulo Variable Classes**. Pre-print.

Arxiv

van der Giessen, I., Jalali, R., & Kuznets, R. **Extensions of K5: Proof Theory and
Uniform Lyndon Interpolation**. 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods(**Tableaux 2023**).

Presentation (Soon) Arxiv Proceedings (Soon)

Cerna, D. M., & Kutsia T. **Anti-unification and Generalization: A Survey**. 32nd International Joint Conference on Artificial Intelligence (**IJCAI 2023**).

Presentation Arxiv Proceedings