Sound generalizations in mathematical induction

International audienceMany proofs by induction diverge without a suitable generalization of the goal to be proved. The aim of the present paper is to propose a method that automatically finds a generalized form of the goal before the induction sub-goals are generated and failure begins. The method works in the case of monomorphic theories (see Section 1). However, in contrast to all heuristic-based methods, our generalization method is sound: A goal is an inductive theorem if and only if its generalization is an inductive theorem. As far as we know this is the first approach that proposes sound generalizations for mathematical induction