Unification algorithm efficiency
The actual implementation of the unification algorithm was made following the first definition in this paper.
But after Section 3 in this paper, more efficient versions of the algorithm are proposed; in some future, will be a good thing to implement the more efficient version proposed.