Skip to Main content Skip to Navigation
Reports

Termination of rewriting under strategies: a generic approach

Isabelle Gnaedig 1 Hélène Kirchner 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We propose a synthesis of three induction based algorithms, we already have given to prove termination of rewrite rule based programs, respectively for the innermost, the outermost and the local strategies. A generic inference principle is presented, based on an explicit induction on the termination property, which genetates ordering constraints, defining the induction relation. The generic inference principle is then instantiated to provide proof procedures for the three specific considered strategies.
Complete list of metadatas

Cited literature [56 references]  Display  Hide  Download

https://hal.inria.fr/inria-00113156
Contributor : Isabelle Gnaedig <>
Submitted on : Friday, November 10, 2006 - 6:56:51 PM
Last modification on : Monday, September 17, 2018 - 1:42:01 PM
Document(s) archivé(s) le : Thursday, September 20, 2012 - 2:40:09 PM

Identifiers

  • HAL Id : inria-00113156, version 1

Collections

Citation

Isabelle Gnaedig, Hélène Kirchner. Termination of rewriting under strategies: a generic approach. [Research Report] 2006. ⟨inria-00113156⟩

Share

Metrics

Record views

272

Files downloads

157