Stratégies de dérivations de programmes logiques
Résumé
Cet article traite de la construction de programmes logiques (programmes en clauses de Horn) et plus particulièrement du problème des eurekas. Dans le processus de transformation de programmes, il est souvent nécessaire d'utiliser certaines propriétés des programmes. Ces propriétés sont appelées eurkas car elle ne sont pas données a priori, ce sont des propriétés intrinsèques aux programmes et c'est l'utilisateur qui doit les découvrir. Le problème est donc crucial, car d'une part sans ces eurekas il n'est pas possible de poursuivre la transformation, d'autre part l'invention de tels eurekas, qui repose sur l'intuition et l'expertise de l'utilisateur, est difficile à automatiser. La technique présentée ici est une tentative d'automatisation de la génération de ces eurekas. Cette technique doit etre considérée comme une contribution à l'automatisation dans le domaine de la construction de programmes par transformation, elle vient donc compléter les nombreuses tactiques existant déjà dans ce domaine.