{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:42:58Z","timestamp":1725486178463},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540430025"},{"type":"electronic","value":"9783540452942"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45294-x_28","type":"book-chapter","created":{"date-parts":[[2007,6,12]],"date-time":"2007-06-12T02:45:12Z","timestamp":1181616312000},"page":"334-346","source":"Crossref","is-referenced-by-count":4,"title":["Rewrite Closure for Ground and Cancellative AC Theories"],"prefix":"10.1007","author":[{"given":"Ashish","family":"Tiwari","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,11,26]]},"reference":[{"key":"28_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-7118-2","volume-title":"Canonical Equational Proofs","author":"L. Bachmair","year":"1991","unstructured":"L. Bachmair. Canonical Equational Proofs. Birkh\u00e4user, Boston, 1991."},{"issue":"2 & 3","key":"28_CR2","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/0304-3975(89)90003-0","volume":"67","author":"L. Bachmair","year":"1989","unstructured":"L. Bachmair and N. Dershowitz. Completion for rewriting modulo a congruence. Theoretical Computer Science, 67(2 & 3):173\u2013201, October 1989.","journal-title":"Theoretical Computer Science"},{"key":"28_CR3","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/174652.174655","volume":"41","author":"L. Bachmair","year":"1994","unstructured":"L. Bachmair and N. Dershowitz. Equational inference, canonical proofs, and proof orderings. Journal of the ACM, 41:236\u2013276, 1994.","journal-title":"Journal of the ACM"},{"unstructured":"L. Bachmair and H. Ganzinger. Ordered chaining calculi for first-order theories of binary relations. Technical Report MPI-I-95-2-009, 1995.","key":"28_CR4"},{"doi-asserted-by":"crossref","unstructured":"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\u2013259. Springer, 2000. LNAI 1794.","key":"28_CR5","DOI":"10.1007\/10720084_16"},{"doi-asserted-by":"crossref","unstructured":"L. Bachmair and A. Tiwari. Abstract congruence closure and specializations. In D. McAllester, editor, CADE, pages 64\u201378. Springer, 2000. LNAI 1831. Full version to appear in J. of Automated Reasoning, http:\/\/www.csl.sri.com\/users\/tiwari\/ .","key":"28_CR6","DOI":"10.1007\/10721959_5"},{"key":"28_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0913-3","volume-title":"Gr\u00f6bner bases: a computational approach to commutative algebra","author":"T. Becker","year":"1993","unstructured":"T. Becker and V. Weispfenning. Gr\u00f6bner bases: a computational approach to commutative algebra. Springer-Verlag, Berlin, 1993."},{"unstructured":"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.","key":"28_CR8"},{"unstructured":"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\u2013359. IEEE Computer Society Press, 1987.","key":"28_CR9"},{"key":"28_CR10","series-title":"Lect Notes Comput Sci","volume-title":"Rewriting Techniques and Applications, RTA-93","year":"1993","unstructured":"C. Kirchner, editor. Rewriting Techniques and Applications, RTA-93, Montreal, Canada, 1993. Springer-Verlag. LNCS 690."},{"key":"28_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/3-540-56868-9_3","volume-title":"Kirchner","author":"A. Levy","year":"1993","unstructured":"A. Levy and J. Agusti. Bi-rewriting, a termrewriting technique for monotone order relations. In Kirchner, pages 17\u201331. LNCS 690."},{"key":"28_CR12","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/BF00289268","volume":"15","author":"E. W. Mayr","year":"1981","unstructured":"E. W. Mayr. Persistence of vector replacement systems is decidable. Acta Informatica 15, pages 309\u2013318, 1981. NewsletterInfo: 8.","journal-title":"Acta Informatica"},{"key":"28_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1007\/3-540-56868-9_30","volume-title":"Kirchner","author":"D. A. Plaisted","year":"1993","unstructured":"D. A. Plaisted. Polynomial time termination and constraint satisfaction tests. In Kirchner [10], pages 405\u2013420. LNCS 690."},{"doi-asserted-by":"crossref","unstructured":"S. Rao Kosaraju. Decidability of reachability in vector addition systems. In Proc. 14th annual ACM symposium on theory of computing, pages 267\u2013281, May 1982.","key":"28_CR14","DOI":"10.1145\/800070.802201"},{"key":"28_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"374","DOI":"10.1007\/3-540-56868-9_28","volume-title":"Kirchner","author":"A. Rubio","year":"1993","unstructured":"A. Rubio and R. Nieuwenhuis. A precedence-based total AC-compatible ordering. In Kirchner [10], pages 374\u2013388. LNCS 690."},{"doi-asserted-by":"crossref","unstructured":"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.","key":"28_CR16","DOI":"10.1007\/3-540-45294-X_28"}],"container-title":["Lecture Notes in Computer Science","FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45294-X_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T01:28:02Z","timestamp":1556501282000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45294-X_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540430025","9783540452942"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-45294-x_28","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}