[Back]

S. Eberhard, S. Hetzl:
"Inductive theorem proving based on tree grammars";
Annals of Pure and Applied Logic, 166 (2015), 6; 665 - 700.

Induction plays a key role in reasoning in many areas of mathematics and computer science. A central problem in the automation of proof by induction is the non-analytic nature of induction invariants. In this paper we present an algorithm for proving universal statements by induction that separates this problem into two phases. The first phase consists of a structural analysis of witness terms of instances of the universal statement. The result of such an analysis is a tree grammar which induces a quantifier-free unification problem which is solved in the second phase. Each solution to this problem is an induction invariant. The arguments and techniques used in this paper heavily exploit a correspondence between tree grammars and proofs already applied successfully to the generation of non-analytic cuts in the setting of pure first-order logic.

Proof theory; Herbrand´s theorem; Inductive theorem proving; Automated deduction

http://dx.doi.org/10.1016/j.apal.2015.01.002