Abstract FR:

Développement d'un outil puissant pour la programmation logique et/ou fonctionnelle et pour la démonstration automatique. L’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 requise par la méthode de preuve par consistance