Completion for Multiple Reduction Orderings

We present a completion procedure (called MKB) that works for multiple reduction orderings. Given equations and a set of reduction orderings, the procedure simulates a computation performed by the parallel processes each of which executes the standard completion procedure (KB) with one of the given orderings. To gain efficiency, however, we develop new inference rules working on objects called nodes, which are data structures consisting of a pair s : t of terms associated with the information to show which processes contain the rule s → t (or t → s) and which processes contain the equation s ↔ t. The idea is based on the observation that some inferences made in different processes are often closely related, so we can design inference rules that simulate these inferences all in a single operation. Our experiments show that MKB is significantly more efficient than the naive simulation of parallel execution of KB procedures, when the number of reduction orderings is large enough....

• Type: Conference
• Year: 1995
• Where: RTA
• Authors: Masahito Kurihara, Hisashi Kondo, Azuma Ohuchi
• Keywords: Completion Procedure, Multiple Reduction Orderings, Reduction Orderings, RTA 1995, Theoretical Computer Science