HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

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.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 7:30:06 PM
Last modification on : Friday, February 4, 2022 - 3:16:33 AM
Long-term archiving on: : Friday, May 13, 2011 - 3:59:55 PM


  • 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⟩



Record views


Files downloads