Transforming infinite rewrite systems into finite rewrite systems by embedding techniques

Abstract

The Knuth-Bendix completion procedure can be used to transform an equational system into a convergent rewrite system. This allows to prove equational and inductive theorems. The main draw back of this technique is that in many cases the completion diverges and so produces an infinite rewrite system. We discuss a method to embed the given specification into a bigger one such that the extended specification allows a finite "parameterized" description of an infinite rewrite system of the base specification. Examples show that in many cases the Knuth-Bendix completion in the extended specification stops with a finite rewrite system though it diverges in the base specification. This indeed allows to prove equational and inductive theorems in the base specification.