Skip to main content
SpringerLink
Log in

Unification theory

  • Conference paper
  • First Online:
Word Equations and Related Topics (IWWERT 1990)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 572))

Included in the following conference series:

Abstract

The purpose of this paper is not to give an overview of the state of art in unification theory. It is intended to be a short introduction into the area of equational unification which should give the reader a feeling for what unification theory might be about. The basic notions such as complete and minimal complete sets of unifiers, and unification types of equational theories are introduced and illustrated by examples. Then we shall describe the original motivations for considering unification (in the empty theory) in resolution theorem proving and term rewriting. Starting with Robinson's first unification algorithm it will be sketched how more efficient unification algorithms can be derived.

We shall then explain the reasons which lead to the introduction of unification in non-empty theories into the above mentioned areas theorem proving and term rewriting. For theory unification it makes a difference whether single equations or systems of equations are considered. In addition, one has to be careful with regard to the signature over which the terms of the unification problems can be built. This leads to the distinction between elementary unification, unification with constants, and general unification (where arbitrary free function symbols may occur). Going from elementary unification to general unification is an instance of the so-called combination problem for equational theories which can be formulated as follows: Let E, F be equational theories over disjoint signatures. How can unification algorithms for E, F be combined to a unification algorithm for the theory E ∪ F.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. F. Baader, “The Theory of Idempotent Semigroups is of Unification Type Zero,” J. Automated Reasoning 2, 1986.

    Google Scholar 

  2. F. Baader, “Unification in Varieties of Idempotent Semigroups,” Semigroup Forum 36, 1987.

    Google Scholar 

  3. F. Baader, “Unification in Commutative Theories,” in C. Kirchner (ed.), Special Issue on Unification, J. Symbolic Computation 8, 1989.

    Google Scholar 

  4. F. Baader, W. Büttner, “Unification in Commutative Idempotent Monoids,” Theoretical Computer Science 56, 1986.

    Google Scholar 

  5. L. Bachmair, Proof Methods for Equational Theories, Ph.D. Thesis, Dep. of Comp. Sci., University of Illinois at Urbana-Champaign, 1987.

    Google Scholar 

  6. L. Baxter, The Complexity of Unification, Ph.D. Thesis, University of Waterloo, Waterloo, Ontario, Canada, 1976.

    Google Scholar 

  7. M. Bidoit, J. Corbin, “A Rehabilitation of Robinson's Unification Algorithm,” In R.E.A. Pavon, editor, Information Processing 83, North Holland, 1983.

    Google Scholar 

  8. A. Boudet, “Unification in a Combination of Equational Theories: An Efficient Algorithm,” Proceedings of the 10th Conference on Automated Deduction, LNCS 449, 1990.

    Google Scholar 

  9. A. Boudet, E. Contejean, H. Devie, “A New AC-unification Algorithm with a New Algorithm for Solving Diophantine Equations,” Proceedings of the 5th IEEE Symposium on Logic in Computer Science, Philadelphia, 1990.

    Google Scholar 

  10. H.-J. Bürckert, “Some Relationships Between Unification, Restricted Unification, and Matching,” Proceedings of the 8th Conference on Automated Deduction, LNCS 230, 1986.

    Google Scholar 

  11. H.-J. Bürckert, A. Herold, M. Schmidt-Schauß, “On Equational Theories, Unification, and Decidability,” in C. Kirchner (ed.), Special Issue on Unification, J. Symbolic Computation 8, 1989.

    Google Scholar 

  12. W. Büttner, “Unification in the Data Structure Multiset,” J. Automated Reasoning 2, 1986.

    Google Scholar 

  13. M. Clausen, A. Fortenbacher, “Efficient Solution of Linear Diophantine Equations,” in C. Kirchner (ed.), Special Issue on Unification, J. Symbolic Computation 8, 1989.

    Google Scholar 

  14. F. Fages, “Associative-Commutative Unification,” Proceedings of the 7th Conference on Automated Deduction, LNCS 170, 1984.

    Google Scholar 

  15. M. Fay, “First Order Unification in an Equational Theory,” Proceedings of the 4th Workshop on Automated Deduction, Austin, Texas, 1979.

    Google Scholar 

  16. A. Fortenbacher, “An Algebraic Approach to Unification under Associativity and Commutativity,” Proceedings of the 1st Conference on Rewriting Techniques and Applications, Dijon, France, LNCS 202, 1985.

    Google Scholar 

  17. M. Franzen, “Hilbert's Tenth Problem Has Unification Type Zero,” Preprint, 1989. To appear in J. Automated Reasoning.

    Google Scholar 

  18. L. Fribourg, “A Narrowing Procedure with Constructors,” Proceedings of the 7th Conference on Automated Deduction, LNCS 170, 1984.

    Google Scholar 

  19. J.H. Gallier, w. Snyder, “A General Complete E-Unification Proceding,” Proceedings of the Second Conference on Rewriting Techniques and Applications, Bordeaux, France, LNCS 256, 1987.

    Google Scholar 

  20. A. Herold, “Combination of Unification Algorithms,” Proceedings of the 8th Conference on Automated Deduction, LNCS 230, 1986.

    Google Scholar 

  21. A. Herold, Combination of Unification Algorithms in Equational Theories, Dissertation, Fachbereich Informatik, Universität Kaiserslautern, 1987.

    Google Scholar 

  22. A. Herold, J.H. Siekmann, “Unification in Abelian Semigroups,” J. Automated Reasoning 3, 1987.

    Google Scholar 

  23. G.P. Huet, Résolution d'équations dans des langages d'ordre 1,2, ...,ω, Thèse d'État, Université de Paris VII, 1976.

    Google Scholar 

  24. G.P. Huet, “Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems,” J. ACM 27, 1980.

    Google Scholar 

  25. F.M. Hullot, “Canonical Forms and Unification,” Proceedings of the 5th Conference on Automated Deduction, LNCS 87, 1980.

    Google Scholar 

  26. J. Jaffar, J.L. Lassez, M. Maher, “A Theory of Complete Logic Programs with Equality,” J. Logic Programming 1, 1984.

    Google Scholar 

  27. J.P. Jouannaud, H. Kirchner, “Completion of a Set of Rules Modulo a Set of Equations,” SIAM J. Computing 15, 1986.

    Google Scholar 

  28. J.P. Jouannaud, C. Kirchner, “Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification,” Preprint, 1990. To appear in the Festschrift to Alan Robinson's birthday.

    Google Scholar 

  29. D. Kapur, P. Narendran, “Complexity of Unification Problems with Associative-Commutative Operators,” Preprint, 1989. To appear in J. Automated Reasoning.

    Google Scholar 

  30. C. Kirchner, Méthodes et Outils de Conception Systématique d'Algorithmes d'Unification dans les Théories equationnelles, Thèse d'Etat, Univ. Nancy, France, 1985.

    Google Scholar 

  31. C. Kirchner, F. Klay, “Syntactic Theories and Unification,” Proceedings of the 5th IEEE Symposium on Logic in Computer Science, Philadelphia, 1990.

    Google Scholar 

  32. K. Knight, “Unification: A Multidisciplinary Survey,” ACM Computing Surveys 21, 1989.

    Google Scholar 

  33. D.E. Knuth, P.B. Bendix, “Simple Word Problems in Universal Algebras,” In J. Leech, editor, Computational Problems in Abstract Algebra, Pergamon Press, Oxford, 1970.

    Google Scholar 

  34. M. Livesey, J.H. Siekmann, “Unification of AC-Terms (bags) and ACI-Terms (sets),” Internal Report, University of Essex, 1975, and Technical Report 3-76, Universität Karlsruhe, 1976.

    Google Scholar 

  35. A. Martelli, U. Montanari, “Theorem Proving with Structure Sharing and Efficient Unification,” Proceedings of International Joint Conference on Artificial Intelligence, 1977.

    Google Scholar 

  36. P. Narendran, F. Otto, “Some Results on Equational Unification,” Proceedings of the 10th Conference on Automated Deduction, LNCS 449, 1990.

    Google Scholar 

  37. A.J. Nevins, “A Human Oriented Logic for Automated Theorem Proving,” J. ACM 21, 1974.

    Google Scholar 

  38. W. Nutt, P. Réty, G. Smolka, “Basic Narrowing Revisited,” J. Symbolic Computation 7, 1989.

    Google Scholar 

  39. M.S. Paterson, M.N. Wegman, “Linear Unification,” J. Comput. Syst. Sci. 16, 1978.

    Google Scholar 

  40. J.P. Pécuchet, Équation avec constantes et algorithme de Makanin, Thèse de Doctorat, Laboratoire d'informatique, Rouen, 1981.

    Google Scholar 

  41. G. Peterson, M. Stickel, “Complete Sets of Reductions for Some Equational Theories,” J. ACM 28, 1981.

    Google Scholar 

  42. G. Plotkin, “Building in Equational Theories,” Machine Intelligence 7, 1972.

    Google Scholar 

  43. J.A. Robinson, “A Machine-Oriented Logic Based on the Resolution Principle,” J. ACM 12, 1965.

    Google Scholar 

  44. J.A. Robinson, “The Unification Computation,” Machine Intelligence 6, 1971.

    Google Scholar 

  45. M. Schmidt-Schauß, “Unification under Associativity and Idempotence is of Type Nullary,” J. Automated Reasoning 2, 1986.

    Google Scholar 

  46. M. Schmidt-Schauß, “Combination of Unification Algorithms,” J. Symbolic Computation 8, 1989.

    Google Scholar 

  47. J.H. Siekmann, “Unification of Commutative Terms,” SEKI-Report, Universität Karlsruhe 1976.

    Google Scholar 

  48. J.H. Siekmann, “Unification Theory: A Survey,” in C. Kirchner (ed.), Special Issue on Unification, Journal of Symbolic Computation 7, 1989.

    Google Scholar 

  49. J.H. Siekmann, P. Szabo, “The Undecidability of the DA-Unification Problem,” SEKI-Report SR-86-19, Universität Kaiserslautern, 1986, and J. Symbolic Logic 54, 1989.

    Google Scholar 

  50. J.R. Slagle, “Automated Theorem Proving for Theories with Simplifiers, Commutativity and Associativity,” J. ACM 21, 1974.

    Google Scholar 

  51. M. Stickel, “A Complete Unification Algorithm for Associative-Commutative Functions,” Proceedings of the International Joint Conference on Artificial Intelligence, 1975.

    Google Scholar 

  52. M.E. Stickel, “A Unification Algorithm for Associative-Commutative Functions,” J. ACM 28, 1981.

    Google Scholar 

  53. M.E. Stickel, “Automated Deduction by Theory Resolution,” J. Automated Reasoning 1, 1985.

    Google Scholar 

  54. E. Tiden, “Unification in Combinations of Collapse Free Theories with Disjoint Sets of Function Symbols,” Proceedings of the 8th Conference on Automated Deduction, LNCS 230, 1986.

    Google Scholar 

  55. E.T. Trajan, “Efficiency of a Good But Not Linear Set Union Algorithm,” J. ACM 22, 1975.

    Google Scholar 

  56. K. Yelick, “Unification in Combinations of Collapse Free Regular Theories,” J. Symbolic Computation 3, 1987.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. German Research Center for AI (DFKI), Postfach 2080, W-6750, Kaiserslautern, Germany

    Franz Baader

Authors
  1. Franz Baader
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

K. U. Schulz

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Baader, F. (1992). Unification theory. In: Schulz, K.U. (eds) Word Equations and Related Topics. IWWERT 1990. Lecture Notes in Computer Science, vol 572. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55124-7_5

Download citation

  • DOI: https://doi.org/10.1007/3-540-55124-7_5

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-55124-9

  • Online ISBN: 978-3-540-46737-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation