Skip to main content
SpringerLink
Log in

Associative-Commutative Unification

  • Conference paper
7th International Conference on Automated Deduction (CADE 1984)

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

Included in the following conference series:

Abstract

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.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  • Baxter L.D. The Complexity of Unification. Ph.D. Thesis, University of Waterloo. (1977)

    Google Scholar 

  • Baxter L.D. The Undecidability of the Third Order Dyadic Unification Problem. Information Control 38, p 170–178, (1978)

    Article  MathSciNet  MATH  Google Scholar 

  • Burstall R.M., Colli. J.S. and Popplestone R.J. Programming in POP-2 Edinburgh University Press. (1971)

    Google Scholar 

  • 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 

  • 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 

  • Davis M. Hilbert’s Tenth Problem is Unsolvable. Amer. Math. Monthly 80,3, pp. 233–289. (1973)

    Article  MathSciNet  MATH  Google Scholar 

  • 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 

  • Fages F. Note sur l’unification des termes de premier ordre finis et infinis. Rapport LITP 83-29. (May 1983)

    Google Scholar 

  • 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 

  • Fay M. First-order Unification in an Equational Theory. 4th Workshop on Automated Deduction, Austin, Texas, pp. 161–167. (Feb. 1979)

    Google Scholar 

  • Goldfarb W.D. The Undecidability of the Second-order Unification Problem. Theoritical Computer Science, vol. 13, pp. 225–230. North Holland Publishing Company. (1981)

    Article  MathSciNet  MATH  Google Scholar 

  • Gordon M.J., Milner A.J. and Wadmworth C.P. Edinburgh LCF. Springer-Verlag LNCS 78. (1979)

    Google Scholar 

  • Gould W.E. A Matching Procedure for Omega Order Logic. Scientific Report 1, AFCRL 66-781, contract AF 19 (628)-3250, (1966)

    Google Scholar 

  • Guard J.R. Automated Logic for Semi-Automated Mathematics. Scientific Report 1, AFCRL 64,411, Contract AF 19 (628)-3250.(1964)

    Google Scholar 

  • 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 

  • Hsiang J. Topics in Automated Theorem Proving and Program Generation. Ph.D. Thesis, Univ. of Illinois at Urbana-Champaign. (Nov. 1982)

    Google Scholar 

  • Huet G. The Undecidability of Unification in Third Order Logic. Information and Control 22, pp. 257–267 (1973)

    Article  MathSciNet  MATH  Google Scholar 

  • Huet G. A Unification Algorithm for Typed λ-Calculus. Theoretical Computer Science 1.1, pp. 27–57. (1975)

    Google Scholar 

  • 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 

  • Huet G. An Algorithm to Generate the Basis of Solutions to Homogenous Linear Diophantine Equations. Information Processing Letters 7,3, pp. 144–147) (1978)

    Article  MATH  Google Scholar 

  • 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 

  • Hullot J.M. Associative-Commutative Pattern Matching, Fifth International Joint Conference on Artificial Intelligence, Tokyo. (1979)

    Google Scholar 

  • 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 

  • Jensen D. and Pietrzykowski T. Mecanizing ω-Order Type Theory through Unification, Theoretical Computer Science 3, pp. 123–171. (1977)

    Article  MATH  Google Scholar 

  • Jouannaud J.P. and Kirchner C. Incremental Construction of Unification Algorithms in Equational Theories. Proc 10th ICALP. (1983)

    Google Scholar 

  • 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 

  • 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 

  • Landin P.J. The Next 700 Programming Languages. CACM 9,3. (March 1988)

    Google Scholar 

  • Lankford D.S. A Unification Algorithm for Abelian Group Theory. Report MTP-1, Math. Dept., Louisiana Tech. U. (Jan. 1979)

    Google Scholar 

  • 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 

  • Livesey M. and Siekmann J. Unification. of Bags and Sets. Internal Report 3/76, Institut fur Informatik I, U. Karlsruhe. (1976)

    Google Scholar 

  • 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 

  • Makanin G.S. The Problem of Solvability of Equations in a Free Semigroup. Akad. Nauk. SSSR, TOM pp. 233,2. (1977)

    Google Scholar 

  • 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 

  • Matiyasevich Y. Diophantine Representation of Recursively Enumerable Predicates. Proceedings of the Second Scandinavian Logic Symposium, North-Holland, (1970)

    Google Scholar 

  • Paterson M.S. and Wegman M.N. Linear Unification. J. of Computer and Systems Sciences 16, pp, 158–167. (1978)

    Article  MathSciNet  MATH  Google Scholar 

  • 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)

    Article  MATH  Google Scholar 

  • Plotkin G. Building-in Equational Theories. Machine Intelligence 7, pp. 73–90. (1972)

    MATH  Google Scholar 

  • 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 

  • 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 

  • Robinson J. A. A Machine Oriented Logic Based on the Resolution Principle. JACM 12, pp. 32–41. (1965)

    Article  MathSciNet  Google Scholar 

  • 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 

  • 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 

  • Siekmann J. Unification and Matching Problems. Ph. P. thesis, Memo CSM-4-78, University of Essex, (1978)

    Google Scholar 

  • Siekmann J. and Szabo P. Universal Unification in Regular Equational ACFM Theories, CADE 6th, New-York. (June 1982)

    Google Scholar 

  • Siagle J.R. Automated Theorem-Proving for Theories with Simplifiers, Commutativity and Associativity. JACM 21, pp. 622–642. (1974)

    Article  MathSciNet  MATH  Google Scholar 

  • Stickel M.E. A Complete Unification Algorithm for Associative-Commutative functions. 4th International Joint Conference on Artificial Intelligence, Tbilisi, (1975)

    Google Scholar 

  • Stickel M.E. Unification Algorithms for Artificial Intelligence Languages. Ph. D. thesis, Carnegie-Mellon University. (1976)

    Google Scholar 

  • Stickel M.E. A Complete Unification Algorithm for Associative-Commutative Functions. JACM 28,3 pp 423–434. (1981)

    Article  MATH  Google Scholar 

  • Venturini-Zilli M. Complexity of the Unification Algorithm for First-Order Expressions. Calcola XII, Fasc. IV, p361–372. (October December 1975)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CNRS, LITP 4 place Jussieu, 75221, Paris Cedex 05

    François Fages

  2. INRIA Domaine de Voluceau Rocquencourt, 78153, Le Chesnay

    François Fages

Authors
  1. François Fages
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. SRI International, 333 Ravenswood Avenue, Menlo Park, CA, 94025, USA

    R. E. Shostak

Rights and permissions

Reprints and permissions

Copyright information

© 1984 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fages, F. (1984). Associative-Commutative Unification. In: Shostak, R.E. (eds) 7th International Conference on Automated Deduction. CADE 1984. Lecture Notes in Computer Science, vol 170. Springer, New York, NY. https://doi.org/10.1007/978-0-387-34768-4_12

Download citation

  • DOI: https://doi.org/10.1007/978-0-387-34768-4_12

  • Publisher Name: Springer, New York, NY

  • Print ISBN: 978-0-387-96022-7

  • Online ISBN: 978-0-387-34768-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation