STRATEGY COMPLIANT MULTI-THREADED TERM COMPLETION

We report on the design, implementation, and performance, of the paral lel term-rewriting system PaReDuX. We discuss the parallelization of t hree term completion procedures: Knuth-Bendix completion, completion m odule AC, and unfailing completion. Our parallelization is strategy-co mpliant, i.e., the parallel code performs exactly the same work as the sequential code, but the work load is shared by many processors. PaRe DuX is designed for shared memory parallel architectures, such as mult i-processor workstations, where it shows good performance on a variety of examples. (C) 1996 Academic Press Limited