Skip to Main content Skip to Navigation
Reports

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 :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00075871
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 7:30:06 PM
Last modification on : Thursday, February 11, 2021 - 2:48:31 PM
Long-term archiving on: : Friday, May 13, 2011 - 3:59:55 PM

Identifiers

  • HAL Id : inria-00075871, version 1

Collections

Citation

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

Share

Metrics

Record views

185

Files downloads

98