Etude et réalisation de méthodes de preuve par récurrence en logique équationnelle

Abstract

L’objet de cette thèse est l’étude pratique de preuve par récurrence en logique équationnelle. Elle fournit ainsi un outil puissant pour la programmation logique et/ou fonctionnelle et pour la démonstration automatique. Notre objectif principal est l’étude et la mise en œuvre d’une méthode de preuve de théorèmes inductifs dans l’algèbre initiale d’une variété équationnelle. La méthode étudiée est la synthèse de la méthode de preuve par consistance et de celle basée sur la réductibilité inductive. Le deuxième objectif est l’étude de la complétude relative, souhaitable dans la conception et la correction des spécifications algébriques structurées et requises par la méthode de preuve par consistance. Une partie de ce travail est consacrée à la présentation de la ω-complétude : elle constitue, à notre connaissance, la première tentative d’étude systématique de cette propriété. Par ailleurs nous donnons une méthode de reconnaissance et de génération des formes normales closes d’un système de réécriture. Enfin il est à noter que toutes ces méthodes de preuves de validité, de complétude relative ainsi que la reconnaissance et la génération des formes normales closes d’un système de réécriture ont été implantées dans le démonstrateur automatique REVE.