Termination of rewriting strategies: a generic approach

Isabelle Gnaedig 1, 2 Hélène Kirchner 1, 2
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 generic termination proof method for rewriting under strategies, based on an explicit induction on the termination property. Rewriting trees on ground terms are modelized by proof trees, generated by alternatively applying narrowing and abstracting steps. The induction principle is applied through the abstraction mechanism, where terms are replaced by variables representing any of their normal forms. The induction ordering is not given a priori, but defined with ordering constraints, incrementally set during the proof. The generic method is then instantiated for the innermost strategy, as an example.
Type de document :
Communication dans un congrès
M. Hofmann, H.-W. Loidl. Proceedings of the third Workshop on Applied Semantics APPSEM'05, Sep 2005, Chiemsee, Germany. 2005
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00172897
Contributeur : Isabelle Gnaedig <>
Soumis le : mardi 18 septembre 2007 - 12:45:33
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58
Document(s) archivé(s) le : vendredi 9 avril 2010 - 02:22:12

Fichier

appsem.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00172897, version 1

Collections

Citation

Isabelle Gnaedig, Hélène Kirchner. Termination of rewriting strategies: a generic approach. M. Hofmann, H.-W. Loidl. Proceedings of the third Workshop on Applied Semantics APPSEM'05, Sep 2005, Chiemsee, Germany. 2005. 〈inria-00172897〉

Partager

Métriques

Consultations de la notice

165

Téléchargements de fichiers

68