Decidable Approximations of Sets of Descendants and Sets of Normal Forms - extended version -

Thomas Genet 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We present here decidable approximations of sets of descendants and sets of normal forms of Term Rewriting Systems, based on specific tree automata techniques. In the context of rewriting logic, a Term Rewriting System is a program, and a normal form is a result of the program. Thus, approximations of sets of descendants and sets of normal forms provide tools for analysing a few properties of programs: we show how to compute a superset of results, to prove the sufficient completeness property, or to find a criterion for proving termination under a specific strategy, the sequential reduction strategy.
Type de document :
Rapport
[Research Report] RR-3325, INRIA. 1997, pp.28
Liste complète des métadonnées

https://hal.inria.fr/inria-00073364
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 12:37:48
Dernière modification le : mardi 24 avril 2018 - 14:12:05
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:43:57

Fichiers

Identifiants

  • HAL Id : inria-00073364, version 1

Collections

Citation

Thomas Genet. Decidable Approximations of Sets of Descendants and Sets of Normal Forms - extended version -. [Research Report] RR-3325, INRIA. 1997, pp.28. 〈inria-00073364〉

Partager

Métriques

Consultations de la notice

186

Téléchargements de fichiers

159