Generalization Heuristics for Theorems Related to Recursively Defined Functions

Book One

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 4

Automated Reasoning

This paper is concerned with the problem of generalizing theorems about recursively defined functions, so as to make these theorems amenable to proof by induction. Some generalization heuristics are presented for certain special forms of theorems about functions specified by certain recursive schemas. The heuristics are based upon the analysis of computational sequences associated with the schemas. If applicable, the heuristics produce generalizations that are guaranteed to be theorems.