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 algorithm¹, RG1 and RG2 algorithms². 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.