Je vais présente mes travaux sur la mécanisation du raisonnement par récurrence et ses applications à la preuve de spécifications, de programmes et de circuits : \noindent {\bf 1. Preuves dans les Théories Conditionnelles :} Il existe essentiellement deux approches pour automatiser le raisonnement par récurrence. La méthode classique demande un schéma de récurrence explicite. Cette méthode échoue souvent car les schémas de récurrence ne rendent pas compte assez fidèlement de la structure du modèle initial. D'autre part les récurrences mutuelles sont difficiles à gérer dans cette approche. De plus, cette méthode ne permet pas la réfutation des conjectures non valides. La seconde technique de preuve, appelée {\em récurrence implicite\/}, consiste à montrer que la conjecture est cohérente avec le modèle initial. La cohérence est détectée par une procédure de complétion. Bien que complète pour la réfutationdes conjectures fausses, elle échoue souvent à cause de la divergence des procédures de complétion. C'est pourquoi nous avons proposé de combiner les aspects positifs des deux techniques précédentes en se fondant sur la notion d'{\em ensemble test}, qui peut être considéré comme une description finie du modèle initial associé à la spécification. Nous avons généralisé cette méthode de preuves par récurrence avec ensemble test pour les théories paramétrées et les théories associatifs et commutatifs. La plupart des procédures et algorithmes issus de nos travaux sont implantés dans le système {\tt SPIKE} à l'aide du langage Objectif Caml. Les principales fonctionnalité de {\tt SPIKE} sont les preuves par récurrence et l'aide à la construction de spécifications correctes. {\tt SPIKE} a permis de prouver plusieurs problèmes difficiles voire inaccessibles pour les autres systèmes d'une manière totalement automatique (arithmétique élémentaire, correction de tris, invariants dans le calcul des situations, \ldots ) ou avec une interaction plus faible qu'avec d'autres systèmes de preuves automatiques comme {\tt NQTHM}, {\tt RRL}, {\tt LP} et {\tt PVS} (tour de carte de Gilbreath, théorème de Ramsey, théorème du binôme, correction de circuits digitaux, etc.). \noindent {\bf 2. Preuves dans les Théories avec Relation d'Appartenance :} La plupart des prouveurs existants considèrent uniquement des spécifications suffisamment complètes sur des constructeurs libres. Le prouveur automatique {\tt SPIKE} n'interdit pas l'utilisation des spécifications avec relations entre les constructeurs mais dans ce cas la complétude réfutationnelle de la procédure de preuves par récurrence n'est plus garantie et l'efficacité du prouveur est très limitée en pratique. Nous avons proposé, en collaboration avec Jean-Pierre Jouannaud (LRI, université Paris Sud), une nouvelle méthode de test de complètude suffisante et de preuves par récurrence dans le cadre de la logique des clauses de Horn avec égalité et relation d'appartenance. Nous avons testé cette méthode à l'aide de quelques exemples (inaccessibles pour les autres systèmes y compris pour {\tt SPIKE}). Ces exemples ont mis en évidence l'efficacité et la simplicitédes preuves obtenues. \noindent {\bf 3. Preuves dans les théories observationnelles :} Pour prouver la correction d'un programme par rapport à une spécification, il est souvent essentiel de faire abstraction de certains détails d'implantation et de considérer seulement le {\em comportement observable} du programme. Bien qu'un grand nombre de travaux aient été consacrés aux aspects sémantiques de l'observabilité, il existe peu d'études sur les techniques de preuves et encore moins d'implantations. Nous avons développé, en collaboration avec N. Berregeb et M. Rusinowitch (INRIA Lorraine), une nouvelle approche pour intégrer la méthode de {\em Context Induction} de Hennicker dans le cadre de la récurrence avec ensembles test. L'aspect le plus original de notre technique est la notion de contexte critique, analogue à celle d'ensemble test, qui permet de schématiser l'ensemble des contextes possibles d'un terme. Les premières expérimentations ont donné des résultats très prometteurs.

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Curation

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002210 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Crin/Curation/biblio.hfd -nk 002210 | SxmlIndent | more

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Crin
   |étape=   Curation
   |type=    RBID
   |clé=     CRIN:bouhoula98a
   |texte=   Mécanisation du Raisonnement par Récurrence
}}