A confluence criterion based on the generalised Newman Lemma

Abstract

In order to improve the efficiency of the Knuth-Bendix Algorithm by eliminating unnecessary reductions, a criterion predicting confluence of critical pairs was given by Winkler in 1983. Subsequently, Winkler and Buchberger also presented a more general form of Newman's Lemma. We derive a more general confluence criterion directly from the Generalised Newman Lemma and integrate it into the Knuth-Bendix Algorithm with the aim of generating fewer critical pairs. With the new criterion it is possible to give a concise justification for the removal of reducible rules in the KB-algorithm. A slightly specialised version of this criterion needs only a single match to test for; empirical results substantiate the claim of a considerable gain in efficiency for the Knuth-Bendix Algorithm.