Unification Algorithms

Abstract

The name unification and the first formal investigation of this notion is due to J.A.Robinson. The notions of unification and most general unifier were independently reinvented by Knuth and Bendix. Various researchers have studied the problem further. Among other results, it was shown that linear time algorithms for unification exist. In this paper, the already existing unification algorithm is modified and improved. Also, an interesting implementation of a new algorithm is presented.