Abstract: 

Proof theory studies systems of rules useful for enumerating valid statements within a target logic. Given an expressive enough proof system, we can translate a ‘mathematical’ proof into a fully formal logic proof explicitly describing every reasoning step. Like mathematical proofs, there may be a variety of formal proofs ending with the same statement. Such proofs are critically important to mathematical practice, providing deep insights into the object of interest. A natural question is, “Can we compare formal proofs?”

Gentzen’s Hauptsatz provides a method for transforming a proof by simplifying the contained lemmas and even eliminating the lemmas altogether, resulting in an analytic proof, i.e. a proof without detours. Effective construction of an analytic proof provides us with Herbrand’s Theorem, a key result providing the foundation for the resolution method and most modern automated reasoning technology. Contemporary investigations into proof transformation led by A. Leitsch and M. Baaz turned this relationship around to show that resolution-based theorem provers allow for effective proof transformation.

However, the transformation methods mentioned above falter in the presence of an inductive argument. While there exist methods transforming proofs containing induction, they cannot reach the analytic proof or a representation of it. Studying proof transformation in the presence of inductive arguments is the central task of the GACR-FWF international project PANDAFOREST. We study resolution-based proof transformation for proofs containing induction to improve our understanding of automated inductive reasoning.

This talk presents our recent work on inductive analogs of classical first-order syntactic unification. We show that it is possible to decide whether a given recursively-defined infinite term unifies with a given finite term. The proof depends on a simple and well-understood unification procedure and shows that there are only finitely many constraints to consider modulo variable renaming. Thus, evoking the pigeonhole principle is enough to close the argument. Our construction closely resembles certain streams, processes, and memory models; thus, we see the possibility of application beyond the scope of the project.

Reference material:

Recursive First-order Syntactic Unification Modulo Variable Classes

Proof analysis AND Automated deduction FOr REcursive STructures (PANDAFOREST)

Schematic Refutations of Formula Schemata