An Efficient Unification Algorithm

   page       BibTeX_logo.png       attach   
Alberto Martelli, Ugo Montanari
ACM Transactions on Programming Languages and Systems 4(2), pp. 258–282
aprile 1982

The unification problem in first-order predicate calculus is described in general terms as the solution of a system of equations, and a nondeterministic algorithm is given. A new unification algorithm, characterized by having the acyclicity test efficiently embedded into it, is derived from the nondeterministic one, and a PASCAL implementation is given. A comparison with other well-known unification algorithms shows that the algorithm described here performs well in all cases.

rivista o collana
book ACM Transactions on Programming Languages and Systems (TOPLAS)