Shematization of infinite sets of rewrite rules. Applications to the divergence of completion processes

Abstract : Infinite sets of rewrite rules may be generated by completion of term rewriting systems or by a narrowing process for solving equations in equational theories. This is a severe limitation to the practical use of these processes. We propose in this paper a formalism to deal with the problem of divergence, namely the definition of melta-rules (rules with meta-variables), together with the derived notions of met-rewriting and meta-narrowing. We show how to use meta-rules for deciding the validity or satisfiability of an equation in the equational theory defined by the infinite set of rules. We define a sound and complete schematization of the infinite set of rules to ensure that the set of meta-rules and the infinite set of rules can be used equivalently.
Type de document :
Rapport
[Research Report] RR-0680, INRIA. 1987
Liste complète des métadonnées

https://hal.inria.fr/inria-00075873
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 19:30:17
Dernière modification le : samedi 17 septembre 2016 - 01:06:54
Document(s) archivé(s) le : vendredi 13 mai 2011 - 16:01:44

Fichiers

Identifiants

  • HAL Id : inria-00075873, version 1

Collections

Citation

Hélène Kirchner. Shematization of infinite sets of rewrite rules. Applications to the divergence of completion processes. [Research Report] RR-0680, INRIA. 1987. 〈inria-00075873〉

Partager

Métriques

Consultations de la notice

78

Téléchargements de fichiers

45