An Ordering Linear Unification Algorithm
In this paper, we present an ordering linear unification algorithm (OLU). A new idea on substitution of the binding terms is introduced to the algorithm, which is able to overcome some drawbacks of other algorithms, e.g., MM algorithm1, RG1 and RG2 algorithms2. Particularly, if we use the directed cyelic graphs, the algorithm needs not check the binding order, then the OLU algorithm can also be applied to the infinite tree data structure, and a higher efficiency can be expected.
The paper focuses upon the discussion of OLU algorithm and a partial order structure with respect to the unification algorithm.
This algorithm has been implemented in the GKD-PROLOG/VAX780 interpreting system. Experimental results have shown that the algorithm is very simple and efficient.