The Knuth-Bendix algorithm in parallel architecture

D. Knuth and P. Bendix (1970) developed an algorithm for transforming a set of equations into a set of simplification rules. This way, an equation t₁=t₂ is true if and only if t₁ and t₂ reduce to the same normal form. The authors implement the algorithm using the Prolog interpreter POPLOG in a Sun 3/160. However, the algorithm is slow since a large number of rules have to be generated, even for the best predefined orderings. If the algorithm is extended to handle conditional equations, then it is even slower. However, the most time-consuming steps can be done in parallel. The authors investigate the use of the parallel architecture of the connection machine and of Sequent Balance 8000 to speed up the algorithm. They use Lisp on the connection machine and Prolog on the Sequent and compare the two architectures as well as the languages as far as the efficiency is concerned