communications de Tunis

In this paper, we develop a new approach for mechanizing induction on complex data structures (like sets, sorted lists, trees, powerlists...). The key idea is to compute a tree grammar with constraints which describes exactly the initial model of the given specification, unlike test sets or cover sets which are approximative induction schemes when the constructors are not free. This grammar is used for the generation of subgoals during the proof by induction. Our procedure is sound and refutationally complete even with constrained axioms for constructors. Our method subsumes all test set induction techniques, and yields very natural proofs for several examples on which other approaches failed.