High-performance permutative completion
James Daniel Christian, Dallas Lankford, Bob Boyer · 1989
Our research has been concerned with improving procedures for completing sets of equations into confluent sets of reductions. First, we have investigated ways to make the Knuth-Bendix completion procedure execute significantly faster, so that completion-based systems can be more readily used for experimentation with difficult problems. Speedups in excess of an order of magnitude have been achieved by using discrimination net indexing techniques and a new data structure for representing first-order terms. Next, we have designed a completion procedure for use with simple linear permutative theories. The procedure is novel in that it dynamically modifies the unification, matching, and termination algorithms to accommodate failure equations. We have developed a new termination algorithm which combines the Knuth-Bendix ordering with the recursive path ordering, and which is suitable for simple linear permutative theories. In addition, we have developed improvements to Claude Kirchner's tools for automatically generating unification algorithms, so that they are more suitable for practical use. The outcome of this research has been a Lisp program called HIPER, which embodies the several ideas developed during our investigation.