An Efficient Unification Algorithm

@article{unification-toplas4,
   abstract = {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.},
   acm = {357169},
   apice = {UnificationToplas4},
   author = {Alberto Martelli and Ugo Montanari},
   doi = {10.1145/357162.357169},
   issn = {0164-0925},
   journal = {ACM Transactions on Programming Languages and Systems},
   month = {April},
   number = 2,
   numpages = 25,
   openalex = {W2113722134},
   pages = {258--282},
   publisher = {ACM},
   title = {An Efficient Unification Algorithm},
   url = {https://dl.acm.org/doi/10.1145/357162.357169},
   volume = 4,
   year = 1982
}