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.