Skip to main content

Part of the book series: Lecture Notes in Networks and Systems ((LNNS,volume 83))

  • 527 Accesses

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 129.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Baader, F., Snyder, W.: Handbook of Automated Reasoning. In: Robinson, A., Voronkov, A. (eds.) Elsevier Science Publishers B.V. (2001)

    Google Scholar 

  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. Robinson, J.A.: A machine oriented logic based on the resolution principle. J. of the ACM 12(1), 23–41 (1965)

    Article  MathSciNet  Google Scholar 

  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. Herbrand, J.: Recherches sur la theorie de la demonstration. In: Goldfarb, W.D. (ed.) Logical Writings. Reidel, Dordrecht (1971)

    Chapter  Google Scholar 

  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. Martelli, A., Montanari, U.: Am efficient unification algorithm. ACM Trans. Program. Lang. Syst. 4(2), 258–282 (1982)

    Article  Google Scholar 

  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)

    MATH  Google Scholar 

  9. Paterson, M.S., Wegman, M.N.: Linear unification. J. Comput. Syst. Sci. 16(2), 158–167 (1978)

    Article  MathSciNet  Google Scholar 

  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 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Mirna Udovicic .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

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

Publish with us

Policies and ethics