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.


  1. 1.
    Baader, F., Snyder, W.: Handbook of Automated Reasoning. In: Robinson, A., Voronkov, A. (eds.) Elsevier Science Publishers B.V. (2001)Google Scholar
  2. 2.
    Baader, F., Siekmann, J.H.: Unification Theory, Handbook of Logic in Artificial Intelligence and Logic Programming, pp. 41–125. Oxford University Press, Oxford, UK (1994)Google Scholar
  3. 3.
    Robinson, J.A.: A machine oriented logic based on the resolution principle. J. of the ACM 12(1), 23–41 (1965)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Herbrand, J.: Investigations in proof theory: the properties of true propositions. In: van Heijenoort, J. (ed.) From Frege to Godel: A Source Book in Mathematical Logic, 1879–1931, pp. 525–581. Harvard University Press, Cambridge, MA (1967)Google Scholar
  5. 5.
    Herbrand, J.: Recherches sur la theorie de la demonstration. In: Goldfarb, W.D. (ed.) Logical Writings. Reidel, Dordrecht (1971)CrossRefGoogle Scholar
  6. 6.
    Martelli, A., Montanari U.: Unification in linear time and space: A structured presentation, Technical Report B76-16, University of Pisa (1976)Google Scholar
  7. 7.
    Martelli, A., Montanari, U.: Am efficient unification algorithm. ACM Trans. Program. Lang. Syst. 4(2), 258–282 (1982)CrossRefGoogle Scholar
  8. 8.
    Knuth, D.E., Bendix, P.B.: Simple words problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra. Pergamon Press, Oxford (1970)zbMATHGoogle Scholar
  9. 9.
    Paterson, M.S., Wegman, M.N.: Linear unification. J. Comput. Syst. Sci. 16(2), 158–167 (1978)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Huet G.P.: Resolution d’equations dans les langages d’ordre 1,2,…,omega, These de doctorat d’etat, Universite Paris VII (1976)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.SSSTSarajevoBosnia and Herzegovina

Personalised recommendations