Skip to Main content Skip to Navigation

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

Cited literature [56 references]  Display  Hide  Download
Contributor : Isabelle Gnaedig Connect in order to contact the contributor
Submitted on : Friday, November 10, 2006 - 6:56:51 PM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM
Long-term archiving on: : Thursday, September 20, 2012 - 2:40:09 PM


  • HAL Id : inria-00113156, version 1



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



Les métriques sont temporairement indisponibles