Associative-Commutative Unification

  • François Fages
Part of the Lecture Notes in Computer Science book series (LNCS, volume 170)


Unification in equational theories, that is solving equations in varieties, is of special relevance to automated deduction. Recent results in term rewriting systems, as in [Peterson and Stickel 81] and [Hsiang 82], depend on unification in presence of associative-commutative functions. Stickel [75,81] gave an associative-commutative unification algorithm, but its termination in the general case was still questioned. Here we give an abstract framework to present unification problems, and we prove the total correctness of Stickel’s algorithm.

The first part of this paper is an introduction to unification theory, The second part is devoted to the associative-commutative ease. The algorithm of Stickel is defined in ML [Gordon, Milner and Wadsworth 79] since in addition to being an effective programming language, ML is a precise and concise formalism close to the standard mathematical notations. The proof of termination and completeness is based on a relatively simple measure of complexity for associative-commutative unification problems.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Baxter L.D. The Complexity of Unification. Ph.D. Thesis, University of Waterloo. (1977)Google Scholar
  2. Baxter L.D. The Undecidability of the Third Order Dyadic Unification Problem. Information Control 38, p 170–178, (1978)MathSciNetCrossRefzbMATHGoogle Scholar
  3. Burstall R.M., Colli. J.S. and Popplestone R.J. Programming in POP-2 Edinburgh University Press. (1971)Google Scholar
  4. Colmerauer A. Prolog II, manuel de référence et modèle théorique, Rapport interne, Groupe d’Intelligence Artificielle, Université d’Aix-Marseille II. (Mars 1982)Google Scholar
  5. Colmerauer K. Kanoui H. and Van Caneghem M. Etude et Réalisation d’un systéme PROLOG. Rapport Interne, GIA, Univ. d’Aix-MarseiUe Luminy. (1972)Google Scholar
  6. Davis M. Hilbert’s Tenth Problem is Unsolvable. Amer. Math. Monthly 80,3, pp. 233–289. (1973)MathSciNetCrossRefzbMATHGoogle Scholar
  7. Fages F. Formes canoniques dons les algèbres booléennes, et application à la démonstration automatique en logique de premier ordre. Thèse, Université de Paris VI. (June 83)Google Scholar
  8. Fages F. Note sur l’unification des termes de premier ordre finis et infinis. Rapport LITP 83-29. (May 1983)Google Scholar
  9. Fages F. and Huet G. Unification and Matching in Equational Theories. CAAP 83, l’Aquila, Italy. Lecture Notes in Computer Science 159. (March 1983)Google Scholar
  10. Fay M. First-order Unification in an Equational Theory. 4th Workshop on Automated Deduction, Austin, Texas, pp. 161–167. (Feb. 1979)Google Scholar
  11. Goldfarb W.D. The Undecidability of the Second-order Unification Problem. Theoritical Computer Science, vol. 13, pp. 225–230. North Holland Publishing Company. (1981)MathSciNetCrossRefzbMATHGoogle Scholar
  12. Gordon M.J., Milner A.J. and Wadmworth C.P. Edinburgh LCF. Springer-Verlag LNCS 78. (1979)Google Scholar
  13. Gould W.E. A Matching Procedure for Omega Order Logic. Scientific Report 1, AFCRL 66-781, contract AF 19 (628)-3250, (1966)Google Scholar
  14. Guard J.R. Automated Logic for Semi-Automated Mathematics. Scientific Report 1, AFCRL 64,411, Contract AF 19 (628)-3250.(1964)Google Scholar
  15. Herbrand J. Recherehes sur la théorie de la démonstration. Thèse, U, de Paris, In: Ecrits logiques de Jacques Herbrand, PUF Paris 1968. (1930)Google Scholar
  16. Hsiang J. Topics in Automated Theorem Proving and Program Generation. Ph.D. Thesis, Univ. of Illinois at Urbana-Champaign. (Nov. 1982)Google Scholar
  17. Huet G. The Undecidability of Unification in Third Order Logic. Information and Control 22, pp. 257–267 (1973)MathSciNetCrossRefzbMATHGoogle Scholar
  18. Huet G. A Unification Algorithm for Typed λ-Calculus. Theoretical Computer Science 1.1, pp. 27–57. (1975)Google Scholar
  19. Huet G. Résolution d’équations dons des langages d’ordre 1,2..., omega. Thèse d’Etat, Université de Paris VII, (1976)Google Scholar
  20. Huet G. An Algorithm to Generate the Basis of Solutions to Homogenous Linear Diophantine Equations. Information Processing Letters 7,3, pp. 144–147) (1978)CrossRefzbMATHGoogle Scholar
  21. Huet G. and Oppen D. Equations and Rewrite Rules: a Survey. In Formal Languages: Perspectives and Open Problems, Ed. Book R., Academic Press. (1980)Google Scholar
  22. Hullot J.M. Associative-Commutative Pattern Matching, Fifth International Joint Conference on Artificial Intelligence, Tokyo. (1979)Google Scholar
  23. Huller J.M. Compilation de Formes Canoniques dons les Théories Equationnelles. Thèse de 3ème cycle, U. de Paris Sud. (Nov. 80)Google Scholar
  24. Jensen D. and Pietrzykowski T. Mecanizing ω-Order Type Theory through Unification, Theoretical Computer Science 3, pp. 123–171. (1977)CrossRefzbMATHGoogle Scholar
  25. Jouannaud J.P. and Kirchner C. Incremental Construction of Unification Algorithms in Equational Theories. Proc 10th ICALP. (1983)Google Scholar
  26. Kirchner H. and Kirchner C. Contribution à la résolution d’équations dons les algèbres fibres et les variétés équationnelles d’algèbres. Thèse de 3ème cycle, Université de Nancy. (Mars 1982)Google Scholar
  27. Knuth D. and Bendix P. Simple Word Problems in Universal Algebras. In Computational Problems in Abstract Algebra, Pergamon Press, pp. 263–297. (1970)Google Scholar
  28. Landin P.J. The Next 700 Programming Languages. CACM 9,3. (March 1988)Google Scholar
  29. Lankford D.S. A Unification Algorithm for Abelian Group Theory. Report MTP-1, Math. Dept., Louisiana Tech. U. (Jan. 1979)Google Scholar
  30. Lankford D.S., Butler G. and Brady B. Abelian Group Unification Algorithms for Elementary Terms. Math. Dept., Louisiana Tech. U., Ruston Louisiana 71272 (1983)Google Scholar
  31. Livesey M. and Siekmann J. Unification. of Bags and Sets. Internal Report 3/76, Institut fur Informatik I, U. Karlsruhe. (1976)Google Scholar
  32. Livesey M., Siekmann J., Szabo P. and Unvericht E. Unification Problems for Combinations of Associativity, Commutativity, Distributivity and Idempotence Axioms. 4th Workshop on Automated Deduction, Austin, Texas, pp. 161–167. (Feb. 1979)Google Scholar
  33. Makanin G.S. The Problem of Solvability of Equations in a Free Semigroup. Akad. Nauk. SSSR, TOM pp. 233,2. (1977)Google Scholar
  34. Martelli A. and Montanari U. An Efficient Unification Algorithm. ACM T.O.P.L.A.S., Vet. 4, No. 2, pp 258–282. (April 1982)Google Scholar
  35. Matiyasevich Y. Diophantine Representation of Recursively Enumerable Predicates. Proceedings of the Second Scandinavian Logic Symposium, North-Holland, (1970)Google Scholar
  36. Paterson M.S. and Wegman M.N. Linear Unification. J. of Computer and Systems Sciences 16, pp, 158–167. (1978)MathSciNetCrossRefzbMATHGoogle Scholar
  37. Peterson G.E. and Stickel M.E. Complete Sets of Reduction for Equational Theories with Complete Unification Algorithms. JACM 28,2 pp 233–264. (1981)CrossRefzbMATHGoogle Scholar
  38. Plotkin G. Building-in Equational Theories. Machine Intelligence 7, pp. 73–90. (1972)zbMATHGoogle Scholar
  39. Raulefs P., Siekmann J., Szabo P., Unvericht E. A Short Survey on the State of the Art in Matching and Unification Problems. Sigsam Bulletin 1979, Vol. 13. (1979)Google Scholar
  40. Reynolds John C. GEDANKEN — A Simple Typeless Language Based on the Principle of Completeness and the Reference Concept. CACM 13,5, pp. 308–319. (May 1970)Google Scholar
  41. Robinson J. A. A Machine Oriented Logic Based on the Resolution Principle. JACM 12, pp. 32–41. (1965)MathSciNetCrossRefGoogle Scholar
  42. Robinson G.A. and Wos L.T. Paramodulation and Theorem Proving in First-order Theories with Equality. Machine intelligence 4, American Elsevier, pp. 135–150. (1989)Google Scholar
  43. Rulifson J.F., Derksen J.A. and Waldinger R.J. QA4: a Procedural Calculus for Intuitive Reasoning. Technical Note 73, A.I. Center, SRI Menlo Park. (Nov. 1972)Google Scholar
  44. Siekmann J. Unification and Matching Problems. Ph. P. thesis, Memo CSM-4-78, University of Essex, (1978)Google Scholar
  45. Siekmann J. and Szabo P. Universal Unification in Regular Equational ACFM Theories, CADE 6th, New-York. (June 1982)Google Scholar
  46. Siagle J.R. Automated Theorem-Proving for Theories with Simplifiers, Commutativity and Associativity. JACM 21, pp. 622–642. (1974)MathSciNetCrossRefzbMATHGoogle Scholar
  47. Stickel M.E. A Complete Unification Algorithm for Associative-Commutative functions. 4th International Joint Conference on Artificial Intelligence, Tbilisi, (1975)Google Scholar
  48. Stickel M.E. Unification Algorithms for Artificial Intelligence Languages. Ph. D. thesis, Carnegie-Mellon University. (1976)Google Scholar
  49. Stickel M.E. A Complete Unification Algorithm for Associative-Commutative Functions. JACM 28,3 pp 423–434. (1981)CrossRefzbMATHGoogle Scholar
  50. Venturini-Zilli M. Complexity of the Unification Algorithm for First-Order Expressions. Calcola XII, Fasc. IV, p361–372. (October December 1975)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • François Fages
    • 1
    • 2
  1. 1.CNRSParis Cedex 05
  2. 2.INRIA Domaine de Voluceau RocquencourtLe Chesnay

Personalised recommendations