REVIEW OF HEURISTICS FOR GENERALIZATION

Proof by induction plays a central role in showing that recursive prog rams satisfy their specification. Sometimes a key step is to generalis e a lemma so that its inductive proof is easier. Existing heuristics f or generalisation for induction are examined. The applicability of heu ristics for generalisation is also examined, and it is shown that the kind of examples on which some of the heuristics work best form a well defined class of problems. A class of generalisation problems is iden tified for which none of the methods work, and directions for future r esearch are provided.