| Résumé | Nous proposons avec Adel Bouhoula une nouvelle approche pour l'automatisation de la récurrence sur des structures de données complexes (telles que listes ordonnées, arbres, powerlists...) spécifiées é l'aide d'équations avec conditions et contraintes. Notre procédure est basée sur l'utilisation d'une grammaires d'arbres à contraintes qui décrit exactement le modèle initial de la spécification donnée. Cette grammaire sert à la fois de schéma de récurrence, pour la génération de sous-buts, et pour des vérifications de cohérence durant les étapes de récurrence.
La procédure proposée est montrée correcte et réfutationellement complète même en présence d'axiomes contraints entre termes constructeurs, et fournit des preuves très naturelles sur un certains nombre d'exemples.
|