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 <>
Submitted on : Wednesday, May 24, 2006 - 7:30:17 PM
Last modification on : Thursday, February 11, 2021 - 2:48:31 PM
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

93

Files downloads

68