HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Reports

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.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00075873
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 7:30:17 PM
Last modification on : Friday, February 4, 2022 - 3:18:44 AM
Long-term archiving on: : Friday, May 13, 2011 - 4:01:44 PM

Identifiers

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

Share

Metrics

Record views

45

Files downloads

19