A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm
Franz Winkler, Bruno Buchberger · ACM SIGSAM Bulletin · 1983
Given a finite set E of multivariate polynomials, the second author's 1965 algorithm constructs a set E' of polynomials such that E and E' generate the same ideal congruence, but E' has the additional property that the congruence can be decided by "reduction to normal forms w.r.t. E'." The two essential ideas of this algorithm are: the consideration of certain "critical pairs" associated with elements in E and the successive "completion" of E by adjoining the difference of normal forms of critical pairs.