Completion of Globally Finite Term Rewriting Systems for Inductive Proofs

Abstract

The Knuth-Bendix Algorithm (KBA) is not able to complete term rewriting systems with cyclic rules such as the commutativity. This kind of rules cause cycles in a reduction chain. This problem may be solved by an extension of the KBA for globally finite term rewriting systems. For a globally finite term rewriting system, cycles may occur in a reduction chain, but for each term there is only a finite set of reductions. A confluent and globally finite term rewriting system R provides a decision procedure for equality induced by R: Two terms are equal iff there is a common term in their reduction sets. This extension requires new methods for testing the global finiteness and a new confluence test, because local confluence does not imply global confluence for globally finite relations. In this paper we give a theoretical framework for this extension. We will show how this theory can be applied to term rewriting systems, if we are mainly interested in the initial algebra which is induced by the set of rules.