The Church-Rosser property in computer algebra and special theorem proving

Publisher Website
Google Scholar
Abstract
An important problem both in computer algebra and special theorem proving in connection with automatic program verification is the calculation of canonical forms with respect to some given side relations. If these side relations can be viewed as a rewrite system which has the Church-Rosser property then a normal form algorithm with respect to this system provides a canonical simplifier. For many computational domains there exists a "completion algorithm" for transforming an arbitrary rewrite system into an equivalent one which has the Church-Rosser property. Improvements to the existing completion algorithms are presented. A very general completion algorithm is described which contains all these various algorithms as special cases. A complexity bound for the Buchberger algorithm for trivariate polynomial equations is derived.

This publication has 0 references indexed in Scilit: