Skip to main content
SpringerLink
Log in
Book cover

International Conference on Foundations of Software Technology and Theoretical Computer Science

FSTTCS 2001: FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science pp 334–346Cite as

Rewrite Closure for Ground and Cancellative AC Theories

  • Conference paper
  • First Online:

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

Abstract

Given a binary relation on the set of ground terms over some signature, we define an abstract rewrite closure for . An abstract rewrite closure can be interpreted as a specialized ground tree transducer (pair of bottom-up tree automata) and can be used to efficiently decide the reachability relation . It is constructed using a completion like procedure. Correctness is established using proof ordering techniques. The procedure is extended, in a modular way, to deal with signatures containing cancellative associative commutative function symbols.

This research was supported in part by the National Science Foundation under grants CCR-9902031 and CCR-0082560, and NASA Langley Research Center under contract NAS1-00079.

This is a preview of subscription content, 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   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. L. Bachmair. Canonical Equational Proofs. Birkhäuser, Boston, 1991.

    MATH  Google Scholar 

  2. L. Bachmair and N. Dershowitz. Completion for rewriting modulo a congruence. Theoretical Computer Science, 67(2 & 3):173–201, October 1989.

    Article  MathSciNet  MATH  Google Scholar 

  3. L. Bachmair and N. Dershowitz. Equational inference, canonical proofs, and proof orderings. Journal of the ACM, 41:236–276, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  4. L. Bachmair and H. Ganzinger. Ordered chaining calculi for first-order theories of binary relations. Technical Report MPI-I-95-2-009, 1995.

    Google Scholar 

  5. L. Bachmair, I.V. Ramakrishnan, A. Tiwari, and L. Vigneron. Congruence closure modulo associativity and commutativity. In Frontiers of Combining Systems, 3rd Intl Workshop FroCoS 2000, pages 245–259. Springer, 2000. LNAI 1794.

    Google Scholar 

  6. L. Bachmair and A. Tiwari. Abstract congruence closure and specializations. In D. McAllester, editor, CADE, pages 64–78. Springer, 2000. LNAI 1831. Full version to appear in J. of Automated Reasoning, http://www.csl.sri.com/users/tiwari/.

  7. T. Becker and V. Weispfenning. Gröbner bases: a computational approach to commutative algebra. Springer-Verlag, Berlin, 1993.

    MATH  Google Scholar 

  8. H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree automata techniques and applications. Available at: http://www.grappa.univ-lille3.fr/tata, 1997.

  9. M. Dauchet, T. Heuillard, P. Lescanne, and S. Tison. Decidability of the confluence of ground termrewriting systems. In Proc IEEE Symposium on Logic in Computer Science, LICS, pages 353–359. IEEE Computer Society Press, 1987.

    Google Scholar 

  10. C. Kirchner, editor. Rewriting Techniques and Applications, RTA-93, Montreal, Canada, 1993. Springer-Verlag. LNCS 690.

    Google Scholar 

  11. A. Levy and J. Agusti. Bi-rewriting, a termrewriting technique for monotone order relations. In Kirchner, pages 17–31. LNCS 690.

    Google Scholar 

  12. E. W. Mayr. Persistence of vector replacement systems is decidable. Acta Informatica 15, pages 309–318, 1981. NewsletterInfo: 8.

    Article  MATH  MathSciNet  Google Scholar 

  13. D. A. Plaisted. Polynomial time termination and constraint satisfaction tests. In Kirchner [10], pages 405–420. LNCS 690.

    Google Scholar 

  14. S. Rao Kosaraju. Decidability of reachability in vector addition systems. In Proc. 14th annual ACM symposium on theory of computing, pages 267–281, May 1982.

    Google Scholar 

  15. A. Rubio and R. Nieuwenhuis. A precedence-based total AC-compatible ordering. In Kirchner [10], pages 374–388. LNCS 690.

    Google Scholar 

  16. A. Tiwari. Rewrite closure for ground and cancellative AC theories. Available: http://www.csl.sri.com/users/tiwari/fsttcs01.html, 2001. Full version of this paper.

Download references

Author information

Authors and Affiliations

  1. SRI International, 333 Ravenswood Ave, Menlo Park, CA, USA

    Ashish Tiwari

Authors
  1. Ashish Tiwari
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Automation, Indian Institute of Science, 560012, Bangalore, India

    Ramesh Hariharan  & V. Vinay  & 

  2. Chennai Mathematical Institute, 92 G.N. Chetty Road, 600 017, Chennai, India

    Madhavan Mukund

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Tiwari, A. (2001). Rewrite Closure for Ground and Cancellative AC Theories. In: Hariharan, R., Vinay, V., Mukund, M. (eds) FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2001. Lecture Notes in Computer Science, vol 2245. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45294-X_28

Download citation

  • DOI: https://doi.org/10.1007/3-540-45294-X_28

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43002-5

  • Online ISBN: 978-3-540-45294-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation