Proving inductive equalities algorithms and implementation

Abstract : The aim of this paper is first to describe an algorithm for testing sufficient completeness and second to present concepts necessary to understand the behavior of an implementation of an automatic prover of inductive properties of functional programs or specifications of abstract data types. These programs or specifications are rewriting systems and relations between constructors are allowed. The method is essentially based on a proof by consistency implemented through a Knuth-Bendix completion, extending the Huet-Hullot approach in many respects. This requires to prove the inductive completeness of the set of relations among the constructors, and the relative (or sufficient) completeness of the definitions of the function. After introducing the concept of inductive completeness, inductively complete theories are presented. On the other hand a test of relative completeness is implemented by an extension of an algorithm that worked only when no relation among constructors existed.
Type de document :
[Research Report] RR-0682, INRIA. 1987
Liste complète des métadonnées
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 19:30:06
Dernière modification le : samedi 17 septembre 2016 - 01:06:54
Document(s) archivé(s) le : vendredi 13 mai 2011 - 15:59:55



  • HAL Id : inria-00075871, version 1



Azzedine Lazrek, Pierre Lescanne, Jean-Jacques Thiel. Proving inductive equalities algorithms and implementation. [Research Report] RR-0682, INRIA. 1987. 〈inria-00075871〉



Consultations de la notice


Téléchargements de fichiers