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.
Type de document :
Rapport
[Research Report] 2006
Liste complète des métadonnées

Littérature citée [56 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00113156
Contributeur : Isabelle Gnaedig <>
Soumis le : vendredi 10 novembre 2006 - 18:56:51
Dernière modification le : jeudi 11 janvier 2018 - 06:19:57
Document(s) archivé(s) le : jeudi 20 septembre 2012 - 14:40:09

Identifiants

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

Partager

Métriques

Consultations de la notice

193

Téléchargements de fichiers

117