Completion of term‐rewriting systems with multiple reduction orderings
Hisashi Kondo, Masahito Kurihara, Azuma Ohuchi · Systems and Computers in Japan · 1996
Abstract The Knuth‐Bendix completion procedure results in one of the following, when the reduction ordering and the set of equations are given: (1) the procedure succeeds by generating a complete term‐rewriting system; (2) the procedure fails by not giving the orientation to an equation by the reduction ordering; and (3) the procedure diverges without being terminated. The success or failure of the completion procedure depends greatly on the reduction ordering. This paper proposes a completion procedure with multiple reduction orderings to reduce the burden of the user in determining the reduction ordering and to prevent the procedure from diverging due to the inadequate reduction ordering. To improve the efficiency, the data called node are used, based on the data structure of ATMS, which is an architecture proposed in the artificial intelligence. The parallel execution of the ordinary completion procedure is simulated under each reduction ordering. The property of ATMS to handle the multiple context is utilized, and the duplication of the inference is avoided by sharing the result of inference among the reduction orderings.