A simplified proof of the characterization theorem for Gröbner-bases

Abstract

In /2/ a certain type of bases ("Gröbner-Bases") for polynomial ideals has been introduced whose usefulness stems from the fact that a number of important computability problems in the theory of polynomial ideals are reducible to the construction of bases of this type. The key to an algorithmic construction of Gröbner-bases is a characterization theorem for Gröbner-bases whose proof in /2/is rather complex.In this paper a simplified proof is given. The simplification is based on two new lemmas that are of some interest in themselves. The first lemma characterizes the congruence relation modulo a polynomial ideal as the reflexive-transitive closure of a particular reduction relation ("M-reduction") used in the definition of Gröbner-bases and its inverse. The second lemma is a lemma on general reduction relations, which allows to guarantee the Church-Rosser property under very weak assumptions.