Skip to main content
SpringerLink
Log in

AC-equation solving

  • Conference paper
  • First Online:
Foundations of Software Technology and Theoretical Computer Science (FSTTCS 1991)

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

  • 136 Accesses

Abstract

Equational Programming is an elegant way to uniformly integrate important features of logic and functional programming. A number of function symbols encountered in such a programming paradigm have the properties of associativity and commutativity (AC for short). It is therefore important to find equation solving strategies which can handle AC operators effectively. In this paper we show that a strict top-down approach extending [Mit90] will not solve the problem in the general case. We then develop a sound and complete strategy for equation solving, which performs better than the conventional approaches using AC-narrowing. Furthermore, we show that by using the AC-rules as constraints while solving the non-AC equations, a number of fruitless (and even infinite) search paths may be eliminated.

Partially supported by the National Science Foundation Grant no. CCR-8900678 while at the University of Delaware.

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. R. Barbuti, Marco Bellia, Giorgio Levi, and M. Martelli. LEAF: a language which integrates logic, equations and functions. In D. DeGroot and G. Lindstrom, editors, Logic Programming: Functions, Relations, and Equations, pages 201–238, Prentice-Hall, Englewood Cliffs, NJ, 1986.

    Google Scholar 

  2. Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 6, North-Holland, Amsterdam, 1990.

    Google Scholar 

  3. Nachum Dershowitz and Z. Manna. Proving Termination with Multiset Orderings. In Communications of the ACM, vol. 22, pages 465–476, August 1979.

    Article  Google Scholar 

  4. Nachum Dershowitz, Subrata Mitra and G. Sivakumar. Equation Solving in Conditional AC-Theories. In Proceedings of the Second International Conference on Algebraic and Logic Programming, Nancy, France, October 1990. Vol. 463 of Lecture Notes in Computer Science, Springer Verlag (1990).

    Google Scholar 

  5. Nachum Dershowitz and David A. Plaisted. Equational programming. In J. E. Hayes, D. Michie, and J. Richards, editors, Machine Intelligence 11: The logic and acquisition of knowledge, chapter 2, pages 21–56, Oxford Press, Oxford, 1988.

    Google Scholar 

  6. Nachum Dershowitz and G. Sivakumar. Goal-directed equation solving. In Proceedings of the Seventh National Conference on Artificial Intelligence, pages 166–170, St. Paul, MN, August 1988.

    Google Scholar 

  7. M. Fay. First-order unification in an equational theory. In Proceedings of the Fourth Workshop on Automated Deduction, pages 161–167, Austin, TX, February 1979.

    Google Scholar 

  8. A. Fortenbacher. An Algebraic Approach to Unification under Associativity and Commutativity. In Proc. of Int. Conference of Rewriting Techniques and Applications, Springer LNCS 202, pages 381–397.

    Google Scholar 

  9. Jean-Marie Hullot. Canonical forms and unification. In R. Kowalski, editor, Proceedings of the Fifth International Conference on Automated Deduction, pages 318–334, Les Arcs, France, July 1980. Vol. 87 of Lecture Notes in Computer Science, Springer, Berlin.

    Google Scholar 

  10. Subrata Mitra. Top-Down Equation Solving and Extensions to Associative and Commutative Theories. Masters thesis, Department of Computer and Information Sciences, University of Delaware, Newark, DE, 1990.

    Google Scholar 

  11. Werner Nutt, Pierre Réty and Gert Smolka. Basic Narrowing Revisited. In J. of Symbolic Computation, (1989) Vol. 7, pages 295–317.

    Google Scholar 

  12. Pierre Réty. Improving basic narrowing techniques. In P. Lescanne, editor, Proceedings of the Second International Conference on Rewriting Techniques and Applications, pages 228–241, Bordeaux, France, May 1987. Vol. 256 of Lecture Notes in Computer Science, Springer, Berlin.

    Google Scholar 

  13. G. Sivakumar. Proofs and Computations in Conditional Equational Theories. PhD thesis, Department of Computer Science, University of Illinois, Urbana, IL, 1989.

    Google Scholar 

  14. Mark E. Stickel. A unification Algorithm for Associative-Commutative Functions. In JACM 28, pages 423–434 (1981).

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Illinois, 61801, Urbana, IL

    Subrata Mitra

  2. Department of Computer Science, Indian Institute of Technology, 400076, Bombay

    G. Sivakumar

Authors
  1. Subrata Mitra
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. G. Sivakumar
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Somenath Biswas Kesav V. Nori

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Mitra, S., Sivakumar, G. (1991). AC-equation solving. In: Biswas, S., Nori, K.V. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1991. Lecture Notes in Computer Science, vol 560. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54967-6_60

Download citation

  • DOI: https://doi.org/10.1007/3-540-54967-6_60

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-54967-3

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation