We have seen in the previous chapter that in some cases completion generates a convergent term rewriting system for a given equational theory, and that such a system can then be used to decide the word problem for this equational theory. A very similar approach has independently been developed in the area of computer algebra, where Gröbner bases are used to decide the ideal congruence and the ideal membership problem in polynomial rings. The close connection to rewriting is given by the fact that Gröbner bases define convergent reduction relations on polynomials, and that the ideal congruence problem can be seen as a word problem. In addition, Buchberger's algorithm, which is very similar to the basic completion procedure presented above, can be used to compute Gröbner bases. In contrast to the situation for term rewriting, however, termination of the reduction relation can always be guaranteed, and Buchberger's algorithm always terminates with success. The purpose of this chapter is, on the one hand, to provide another example for the usefulness of the rewriting and completion approach introduced above. On the other hand, the basic definitions and results from the area of Gröbner bases are presented using the notations and results for abstract reduction systems introduced in Chapter 2.

The ideal membership problem

Let us first introduce the basic algorithmic problems that can be solved with the help of Gröbner bases.