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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Baader, F., Snyder, W.: Handbook of Automated Reasoning. In: Robinson, A., Voronkov, A. (eds.) Elsevier Science Publishers B.V. (2001)
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)
Robinson, J.A.: A machine oriented logic based on the resolution principle. J. of the ACM 12(1), 23–41 (1965)
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)
Herbrand, J.: Recherches sur la theorie de la demonstration. In: Goldfarb, W.D. (ed.) Logical Writings. Reidel, Dordrecht (1971)
Martelli, A., Montanari U.: Unification in linear time and space: A structured presentation, Technical Report B76-16, University of Pisa (1976)
Martelli, A., Montanari, U.: Am efficient unification algorithm. ACM Trans. Program. Lang. Syst. 4(2), 258–282 (1982)
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)
Paterson, M.S., Wegman, M.N.: Linear unification. J. Comput. Syst. Sci. 16(2), 158–167 (1978)
Huet G.P.: Resolution d’equations dans les langages d’ordre 1,2,…,omega, These de doctorat d’etat, Universite Paris VII (1976)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Udovicic, M. (2020). Unification Algorithms. In: Avdaković, S., Mujčić, A., Mujezinović, A., Uzunović, T., Volić, I. (eds) Advanced Technologies, Systems, and Applications IV -Proceedings of the International Symposium on Innovative and Interdisciplinary Applications of Advanced Technologies (IAT 2019). IAT 2019. Lecture Notes in Networks and Systems, vol 83. Springer, Cham. https://doi.org/10.1007/978-3-030-24986-1_48
Download citation
DOI: https://doi.org/10.1007/978-3-030-24986-1_48
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-24985-4
Online ISBN: 978-3-030-24986-1
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)