A practically efficient and almost linear unification algorithm (Q1105360)

An efficient unification algorithm for first-order terms is described. It relies on the known theoretical framework of homogeneous and valid equivalence relations on terms and it makes use of a union-find algorithmic schema, thus keeping an almost linear worst-case complexity. Its advantages over similar algorithms are a very low overhead and practical efficiency, even for small terms, that are due to simple data structures and careful design tradeoffs. The proposed algorithm is described in detail such as to be easily implemented. Its main part is proved, and its complexity analyzed. Comparative experimental results that support its advantage are given.