“A parallel completion procedure for term rewriting systems”

Katherine A. Yelick and Stephen J. Garland

Eleventh International Conference on Automated Deduction, Lecture Notes in Computer Science, pages 109–123, Sarasota Springs, NY, June 1992. Springer-Verlag.

We present a parallel completion procedure for term rewriting systems. Despite an extensive literature concerning the well-known sequential Knuth-Bendix completion procedure, little attention has been devoted to designing parallel completion procedures. Because naive parallelizations of sequential procedures lead to over-synchronization and poor performance, we employ a transition-based approach that enables more effective parallelizations. The approach begins with a formulation of the completion procedure as a set of transitions (in the style of Bachmair, Dershowitz, and Hsiang) and proceeds to a highly tuned parallel implementation that runs on a shared memory multiprocessor. The implementation performs well on a number of standard examples.

Back to Publications of Stephen J. Garland