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 metadatas

Cited literature [56 references]  Display  Hide  Download
Contributor : Isabelle Gnaedig <>
Submitted on : Friday, November 10, 2006 - 6:56:51 PM
Last modification on : Monday, September 17, 2018 - 1:42:01 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⟩



Record views


Files downloads