Schematization methods for theorem proving
Méthodes de schématisation pour la démonstration automatique
Abstract
Not available
Ce travail se situe dans le cadre de la déduction automatique. Il traite d'une méthode, appelée la schématisation, utilisée pour remédier à des problèmes d'expressivité, d'efficacité et de divergence. La schématisation est un moyen de représentation finie d'ensembles infinis d'objets. Ceux-ci peuvent se retrouver dans différents domaines de l'informatique. Le but de notre travail est l'étude de cette méthode d'un point de vue théorique et pratique. D’un point de vue théorique, nous avons situé les classes de schématisation existantes dans la hiérarchie des langages d'arbres après les avoir comparé entre elles. Chose qui nous a permis de proposer des classes plus expressives que toutes les classes proposées jusqu'ici et qui sont intéressantes pour la déduction automatique. D’un point de vue pratique, nous avons proposé plusieurs algorithmes de manipulation de schématisations. Nous avons surtout introduit la notion de problème d'inclusion pour lequel nous avons donné un algorithme que nous avons applique à la généralisation inductive d'ensembles infinis de termes. Cet algorithme peut trouver d'autres applications dans le génie logiciel, la réécriture et le calcul des processus. Nous avons ensuite améliore l'algorithme classique de généralisation inductive dans ses cas d'échec en utilisant les I-termes puis les B-termes. Les algorithmes proposés peuvent être vus comme des procédures de construction automatique, respectivement, des I-termes et des B-termes.