Skip to main content
SpringerLink
Log in
Book cover

International Conference on Automated Deduction

CADE 1988: 9th International Conference on Automated Deduction pp 358–367Cite as

Adventures in associative-commutative unification (A summary)

  • Conference paper
  • First Online:

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

Abstract

We have discovered an efficient algorithm for matching and unification in associative-commutative (AC) and associative-commutative-idempotent (ACI) equational theories. In most cases of AC unification and in all cases of ACI unification our method obviates the need for solving diophantine equations, and thus avoids one of the bottlenecks of other associative-commutative unification techniques. The algorithm efficiently utilizes powerful constraints to eliminate much of the search involved in generating valid substitutions. Moreover, it is able to generate solutions lazily, enabling its use in an SLD-resolution-based environment like Prolog. We have found the method to run much faster and use less space than other associative-commutative unification procedures on many commonly encountered AC problems.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Wolfram Büttner. “Unification in Datastructure Multisets”. Journal of Automated Reasoning, 2 (1986) 75–88.

    Article  Google Scholar 

  2. Jim Christian and Pat Lincoln “Adventures in Associative-Commutative Unification” MCC Technical Report Number ACA-ST-275-87, Microelectronics and Computer Technology Corp., Austin, TX, Oct 1987.

    Google Scholar 

  3. François Fages. “Associative-Commutative Unification”. Proceedings 7th International Conference on Automated Deduction, Springer-Verlag. Lecture Notes in Computer Science, Napa Valley, (California), 1984.

    Google Scholar 

  4. Albrecht Fortenbacher. “An Algebraic Approach to Unification Under Associativity and Commutativity” Rewriting Techniques and Applications, Dijon, France, May 1985, ed Jean-Pierre Jouannaud. Springer-Verlag Lecture Notes in Computer Science Vol. 202, (1985) pp. 381–397

    Google Scholar 

  5. P. Gordan, “Ueber die Auflösung linearer Gleichungen mit reelen Coefficienten”. Mathematische Annalen, VI Band, 1 Heft (1873), 23–28.

    Article  MathSciNet  Google Scholar 

  6. Thomas Guckenbiehl and Alexander Herold. “Solving Linear Diophantine Equations”. Universitat Kaiserslautern, Fachbereich Informatik, Postfach 3049, 6750 Kaiserslautern.

    Google Scholar 

  7. Gérard Huet. “An Algorithm to Generate the Basis of Solutions to Homogeneous Linear Diophantine Equations”. IRIA Research Report No. 274, January 1978.

    Google Scholar 

  8. Gérard Huet and D.C.Oppen. “Equations and Rewrite Rules: a Survey”. In Formal Languages: Perspectives and Open Problems, ed R. Book, Academic Press, 1980.

    Google Scholar 

  9. J.M. Hullot. “Associative Commutative Pattern Matching”. Proceedings IJCAI-79, Volume One, pp406–412, Tokyo, August 1979.

    Google Scholar 

  10. Deepak Kapur, G. Sivakumar, H. Zhang. “RRL: A Rewrite Rule Laboratory”. Proceedings of CADE-8, pp 691–692, Oxford, England, 1986.

    Google Scholar 

  11. Claude Kirchner. “Methods and Tools for Equational Unification”. in Proceedings of the Colloquium on the Resolution of Equations in Algebraic Structures, May 1987, Austin, Texas.

    Google Scholar 

  12. Dallas Lankford. “New Non-negative Integer Basis Algorithms for Linear Equations with Integer Coefficients”. May 1987. Unpublished. Available from the author, 903 Sherwood Drive, Ruston, LA 71270.

    Google Scholar 

  13. M. Livesey and J. Siekmann. “Unification of A + C-terms (bags) and A + C + I-terms (sets)”. Intern. Ber. Nr. 5/76, Institut für Informatik I, Unifersität Karsruhe, 1976.

    Google Scholar 

  14. A. Martelli and U. Montanari. “An Efficient Unification Algorithm”. ACM Transactions on Programming Languages and Systems, 4(2):258–282, 1982.

    Article  Google Scholar 

  15. Mark Stickel. “A complete unification algorithm for associative-commutative functions” Proc. 4th IJCAI, Tbilisi (1975), pp.71–82.

    Google Scholar 

  16. Mark Stickel. “A Unification Algorithm for Associative-Commutative Functions”. JACM, Vol.28, No.3, July 1981, pp.423–434.

    Article  Google Scholar 

  17. Mark Stickel. “A Comparison of the Variable-Abstraction and Constant-Abstraction methods for Associative-Commutative Unification” Journal of Automated Reasoning, Sept 1987, pp.285–289.

    Google Scholar 

  18. Hantao Zhang “An Efficient Algorithm for Simple Diophantine Equations”, Tech. Rep. 87–26, Dept. of Computer Science, RPI, 1987.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. MCC, Systems Languages, 3500 W. Balcones Cntr. Dr., 78759, Austin, TX

    Patrick Lincoln & Jim Christian

Authors
  1. Patrick Lincoln
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jim Christian
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Ewing Lusk Ross Overbeek

Rights and permissions

Reprints and permissions

Copyright information

© 1988 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lincoln, P., Christian, J. (1988). Adventures in associative-commutative unification (A summary). In: Lusk, E., Overbeek, R. (eds) 9th International Conference on Automated Deduction. CADE 1988. Lecture Notes in Computer Science, vol 310. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0012843

Download citation

  • DOI: https://doi.org/10.1007/BFb0012843

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-19343-2

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation