{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:23:37Z","timestamp":1725488617041},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540671909"},{"type":"electronic","value":"9783540465089"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46508-1_3","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T20:02:03Z","timestamp":1186171323000},"page":"39-61","source":"Crossref","is-referenced-by-count":6,"title":["Proving Associative-Commutative Termination Using RPO-Compatible Orderings"],"prefix":"10.1007","author":[{"given":"Deepak","family":"Kapur","sequence":"first","affiliation":[]},{"given":"G.","family":"Sivakumar","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/S0747-7171(85)80019-5","volume":"1","author":"L. Bachmair","year":"1985","unstructured":"Bachmair, L., and Plaisted, D.A. (1985): Termination orderings for associative-commutative rewriting systems. J. Symbolic Computation, 1, 329\u2013349","journal-title":"J. Symbolic Computation"},{"issue":"2","key":"3_CR2","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1016\/0167-6423(87)90030-X","volume":"9","author":"A. Ben Cherifa","year":"1987","unstructured":"Ben Cherifa, A., and Lescanne, P. (1987): Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming, 9,2, 137\u2013160.","journal-title":"Science of Computer Programming"},{"key":"3_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/3-540-56868-9_29","volume-title":"Proc. of 5th Intl. Conf. on Rewrite Techniques and Applications (RTA-93)","author":"C. Delor","year":"1993","unstructured":"Delor, C., Puel, L. (1993): Extension of the associative path ordering to a chain of associative commutative symbols. Proc. of 5th Intl. Conf. on Rewrite Techniques and Applications (RTA-93), LNCS, Springer-Verlag, 389\u2013404."},{"key":"3_CR4","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"Dershowitz, N. (1987): Termination of rewriting. J. Symbolic Computation, 3, 69\u2013116.","journal-title":"J. Symbolic Computation"},{"key":"3_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/3-540-16780-3_79","volume-title":"Proc. of 8th Intl. Conf. on Automated Deduction (CADE-8)","author":"I. Gnaeding","year":"1986","unstructured":"Gnaeding, I., and Lescanne, P. (1986): Proving termination of associative-commutative rewriting systems by rewriting. Proc. of 8th Intl. Conf. on Automated Deduction (CADE-8), Oxford, LNCS 230 (ed. Siekmann), Springer Verlag, 52\u201360."},{"key":"3_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/3-540-60692-0_51","volume-title":"Proc. of 15th Conf. on Foundations of Software Technology and Theoretical Computer Science","author":"D. Kapur","year":"1995","unstructured":"Kapur, D., and Sivakumar, G. (1995): Maximal extensions of simplification orderings. Proc. of 15th Conf. on Foundations of Software Technology and Theoretical Computer Science (ed. Thiagarajan), Bangalore, India, Springer Verlag LNCS 1026, 225\u2013239, Dec. 1995."},{"key":"3_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/3-540-62950-5_67","volume-title":"Proc. Rewriting Techniques and Applications, 8th Intl. Conf., RTA-97","author":"D. Kapur","year":"1997","unstructured":"Kapur, D., and Sivakumar, G. (1997): A total ground path ordering for proving termination of AC-Rewrite systems. Proc. Rewriting Techniques and Applications, 8th Intl. Conf., RTA-97, Sitges, Spain, June 1997, Springer LNCS 1231 (ed. H. Comon), 142\u2013156."},{"key":"3_CR8","volume-title":"A recurive path ordering for proving associative-commutative termination","author":"D. Kapur","year":"1998","unstructured":"Kapur, D., and Sivakumar, G.: A recurive path ordering for proving associative-commutative termination Technical Report, Department of Computer Science, State University of New York, Albany, NY, May 1998."},{"key":"3_CR9","unstructured":"Kapur, D., Sivakumar, G. and Zhang, H. (1995): A new ordering for proving termination of AC-rewrite systems. J. Automated Reasoning, 1995."},{"issue":"2","key":"3_CR10","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/0898-1221(94)00218-A","volume":"29","author":"D. Kapur","year":"1995","unstructured":"Kapur, D., and Zhang, H. (1995): An overview of Rewrite Rule Laboratory (RRL). J. Computer and Mathematics with Applications, 29,2, 91\u2013114.","journal-title":"J. Computer and Mathematics with Applications"},{"key":"3_CR11","unstructured":"Lankford, D.S. (1979): On proving term rewriting systems are Noetherian. Memo MTP-3, Lousiana State University."},{"key":"3_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/3-540-53904-2_115","volume-title":"Proc. of 4th Intl. Conf. on Rewrite Techniques and Applications (RTA-91)","author":"P. Narendran","year":"1991","unstructured":"Narendran, P., and Rusinowitch, M. (1991): Any ground associative commutative theory has a finite canonical system. In Book, R. (ed.) Proc. of 4th Intl. Conf. on Rewrite Techniques and Applications (RTA-91), LNCS 488, 423\u2013434."},{"key":"3_CR13","volume-title":"A total AC-compatible ordering with RPO scheme","author":"A. Rubio","year":"1997","unstructured":"Rubio, A. (1997): A total AC-compatible ordering with RPO scheme. Technical Report, Technical Univ. of Catalonia, Barcelona, Spain."},{"key":"3_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"374","DOI":"10.1007\/3-540-56868-9_28","volume-title":"Proc. of 5th Intl. Conf. on Rewrite Techniques and Applications (RTA-93)","author":"A. Rubio","year":"1993","unstructured":"Rubio, A., Nieuwenhuis, R. (1993): A precedence-based total AC-compatible ordering. In Kirchner, C. (ed.) Proc. of 5th Intl. Conf. on Rewrite Techniques and Applications (RTA-93), LNCS Springer-Verlag, 374\u2013388."},{"key":"3_CR15","series-title":"Seki-Report","volume-title":"Path and decomposition orderings for proving AC-termination","author":"J. Steinbach","year":"1989","unstructured":"Steinbach, J. (1989): Path and decomposition orderings for proving AC-termination. Seki-Report, SR-89-18, University of Kaiserslautern. See also \u201cImproving associative path orderings,\u201d in: Proc. of 10th Intl. Conf. on Automated Deduction (CADE-10), Kaiserslautern, LNCS 449 (ed. Stickel), 411\u2013425."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction in Classical and Non-Classical Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46508-1_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,20]],"date-time":"2019-02-20T19:23:52Z","timestamp":1550690632000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46508-1_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540671909","9783540465089"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-46508-1_3","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}