S. Eberhard, S. Hetzl:
"Inductive theorem proving based on tree grammars";
Annals of Pure and Applied Logic,
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
"Offizielle" elektronische Version der Publikation (entsprechend ihrem Digital Object Identifier - DOI)
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.