{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T02:05:05Z","timestamp":1648951505257},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2006,12,2]],"date-time":"2006-12-02T00:00:00Z","timestamp":1165017600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2007,1,23]]},"DOI":"10.1007\/s10817-006-9053-y","type":"journal-article","created":{"date-parts":[[2006,12,1]],"date-time":"2006-12-01T06:51:15Z","timestamp":1164955875000},"page":"205-229","source":"Crossref","is-referenced-by-count":2,"title":["Elimination Transformations for Associative\u2013Commutative Rewriting Systems"],"prefix":"10.1007","volume":"37","author":[{"given":"Kusakari","family":"Keiichirou","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nakamura","family":"Masaki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Toyama","family":"Yoshihito","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,12,2]]},"reference":[{"key":"9053_CR1","unstructured":"Arts, T.: Automatically proving termination and innermost normalization of term rewriting systems. Ph.D. thesis, Utrecht University, Utrecht, The Netherlands (1997)"},{"key":"9053_CR2","first-page":"261","volume-title":"Proc. 7th Int. Joint Conf. on Theory and Practice of Software Development, LNCS 1214 (TAPSOFT\u201997)","author":"T. Arts","year":"1997","unstructured":"Arts, T., Giesl, J.: Automatically proving termination where simplification orderings fail. In: Proc. 7th Int. Joint Conf. on Theory and Practice of Software Development, LNCS 1214 (TAPSOFT\u201997), pp. 261\u2013272. Springer, Berlin Heidelberg New York (1997)"},{"key":"9053_CR3","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/S0304-3975(99)00207-8","volume":"236","author":"T. Arts","year":"2000","unstructured":"Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comp. Sci. 236, 133\u2013178 (2000)","journal-title":"Theor. Comp. Sci."},{"key":"9053_CR4","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, New York (1998)"},{"key":"9053_CR5","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1016\/S0747-7171(85)80019-5","volume":"1","author":"T. Bachmair","year":"1985","unstructured":"Bachmair, T., Plaisted, D.A.: Termination orderings for associative\u2013commutative rewriting systems. J. Symb. Comput. 1, 329\u2013349 (1985)","journal-title":"J. Symb. Comput."},{"key":"9053_CR6","unstructured":"Contejean, E., March\u00e9 C., Monate, B., Urbain, X.: CiME version 2, 2000. (Available at http:\/\/cime.lri.fr\/ )"},{"key":"9053_CR7","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"Dershowitz, N.: Orderings for term-rewriting systems. Theor. Comp. Sci. 17, 279\u2013301 (1982)","journal-title":"Theor. Comp. Sci."},{"key":"9053_CR8","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/3-540-60249-6_56","volume-title":"Proc. 10th Int. Conf. on Fundamentals of Computation Theory, LNCS 965 (FCT\u201995)","author":"M. Ferreira","year":"1995","unstructured":"Ferreira, M., Zantema, H.: Dummy elimination: making termination easier. In: Proc. 10th Int. Conf. on Fundamentals of Computation Theory, LNCS 965 (FCT\u201995), pp. 243\u2013252. Dresden, Germany. Springer, Berlin Heidelberg New York (1995)"},{"key":"9053_CR9","unstructured":"Ferreira, M.: Termination of term rewriting, well-foundedness, totality and transformations. Ph.D. thesis, Utrecht University, Utrecht, The Netherlands (1995)"},{"key":"9053_CR10","doi-asserted-by":"crossref","unstructured":"Ferreira, M., Kesner, D., Puel, L.: Reducing AC-termination to termination. In: Proc. 23rd Int. Symp. on Mathematical Foundations of Computer Science, LNCS 1450 (MFCS\u201998), pp. 239\u2013247 (1998)","DOI":"10.1007\/BFb0055773"},{"key":"9053_CR11","first-page":"309","volume-title":"Proc. 17th Int. Conf. on Automated Deduction, LNAI 1831 (CADE2000)","author":"J. Giesl","year":"2000","unstructured":"Giesl, J., Middeldorp, A.: Eliminating dummy elimination. In: Proc. 17th Int. Conf. on Automated Deduction, LNAI 1831 (CADE2000), pp. 309\u2013323. Pittsburgh, PA. Springer, Berlin Heidelberg New York (2000)"},{"key":"9053_CR12","first-page":"93","volume-title":"Proc. 12th Int. Conf. on Rewriting Techniques and Applications, LNCS 2051 (RTA\u201901)","author":"J. Giesl","year":"2001","unstructured":"Giesl, J., Kapur, D.: Dependency pairs for equational rewriting. In: Proc. 12th Int. Conf. on Rewriting Techniques and Applications, LNCS 2051 (RTA\u201901), pp. 93\u2013107. Utrecht, The Netherlands. Springer, Berlin Heidelberg New York (2001)"},{"issue":"1","key":"9053_CR13","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1006\/jsco.2002.0541","volume":"34","author":"J. Giesl","year":"2002","unstructured":"Giesl, J., Arts, T., Ohlebusch, E.: Modular termination proofs for rewriting using dependency pairs. J. Symb. Comput. 34(1), 21\u201358 (2002)","journal-title":"J. Symb. Comput."},{"key":"9053_CR14","first-page":"165","volume-title":"Proc. 10th Int. Conf. on Logic for Programming Artificial Intelligence and Reasoning, LNAI 2850 (LPAR03)","author":"J. Giesl","year":"2003","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Improving dependency pairs. In: Proc. 10th Int. Conf. on Logic for Programming Artificial Intelligence and Reasoning, LNAI 2850 (LPAR03), pp. 165\u2013179. Almaty, Kazakhstan. Springer, Berlin Heidelberg New York (2003)"},{"key":"9053_CR15","first-page":"210","volume-title":"Proc. 15th Int. Conf. on Rewriting Techniques and Applications, LNCS 3091 (RTA04)","author":"J. Giesl","year":"2004","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Automated termination proofs with AProVE. In: Proc. 15th Int. Conf. on Rewriting Techniques and Applications, LNCS 3091 (RTA04), pp. 210\u2013220. Aachen, Germany. Springer, Berlin Heidelberg New York (2004)"},{"issue":"1,2","key":"9053_CR16","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1016\/j.ic.2004.10.004","volume":"199","author":"N. Hirokawa","year":"2005","unstructured":"Hirokawa, N., Middeldorp, A.: Automating the dependency pair method. Inf. Comput. 199(1,2), 172\u2013199 (2005)","journal-title":"Inf. Comput."},{"key":"9053_CR17","first-page":"1","volume-title":"Term rewriting systems. Handbook of Logic in Computer Science II","author":"J.W. Klop","year":"1992","unstructured":"Klop, J.W.: Term rewriting systems. Handbook of Logic in Computer Science II, pp. 1\u2013112. Oxford University Press, London, UK (1992)"},{"key":"9053_CR18","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1016\/0304-3975(92)90015-8","volume":"103","author":"M. Kurihara","year":"1992","unstructured":"Kurihara, M., Ohuchi, A.: Modularity of simple termination of term rewriting systems with shared constructors. Theor. Comp. Sci., 103, 273\u2013282 (1992)","journal-title":"Theor. Comp. Sci."},{"key":"9053_CR19","first-page":"65","volume":"41","author":"K. Kusakari","year":"2000","unstructured":"Kusakari, K., Toyama, Y.: On proving AC-termination by argument filtering method. IPSJ Trans. Program. 41, No. SIG 4 (PRO 7), 65\u201378 (2000)","journal-title":"IPSJ Trans. Program."},{"issue":"5","key":"9053_CR20","first-page":"604","volume":"E84-D","author":"K. Kusakari","year":"2001","unstructured":"Kusakari, K., Toyama, Y.: On proving AC-termination by AC-dependency pairs. IEICE Trans. Info. Syst. E84-D(5), 604\u2013612 (2001)","journal-title":"IEICE Trans. Info. Syst."},{"key":"9053_CR21","doi-asserted-by":"crossref","unstructured":"March\u00e9, C., Urbain, X.: Termination of associative\u2013commutative rewriting by dependency pairs. In: Proc. 9th Int. Conf. on Rewriting Techniques and Applications, LNCS 1379 (RTA\u201998), pp. 241\u2013255. Tsukuba, Japan (1998)","DOI":"10.1007\/BFb0052374"},{"issue":"1","key":"9053_CR22","doi-asserted-by":"crossref","first-page":"873","DOI":"10.1016\/j.jsc.2004.02.003","volume":"38","author":"C. March\u00e9","year":"2004","unstructured":"March\u00e9, C., Urbain, X.: Modular and incremental proofs of AC-termination. J. Symb. Comput. 38(1), 873\u2013897 (2004)","journal-title":"J. Symb. Comput."},{"key":"9053_CR23","doi-asserted-by":"crossref","unstructured":"Middeldorp, A., Ohsaki, H., Zantema, H.: Transforming termination by self-labeling. In: Proc. 13th Int. Conf. on Automated Deduction, LNCS 1104 (CADE-13), pp. 373\u2013387 (1996)","DOI":"10.1007\/3-540-61511-3_101"},{"key":"9053_CR24","doi-asserted-by":"crossref","unstructured":"Middeldorp, A.: Approximating dependency graphs using tree automata techniques. In: Proc. Int. Joint Conf. on Automated Reasoning, LNAI 2083 (IJCAR01), pp. 593\u2013610. Siena, Italy (2001)","DOI":"10.1007\/3-540-45744-5_49"},{"issue":"10","key":"9053_CR25","first-page":"1225","volume":"J82-D-I","author":"M. Nakamura","year":"1999","unstructured":"Nakamura, M., Kusakari, K., Toyama, Y.: On proving termination by general dummy elimination. IEICE Trans. Info. Syst. J82-D-I(10), 1225\u20131231 (1999) (in Japanese)","journal-title":"IEICE Trans. Info. Syst."},{"key":"9053_CR26","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3661-8","volume-title":"Advanced Topics in Term Rewriting","author":"E. Ohlebusch","year":"2002","unstructured":"Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, Berlin Heidelberg New York (2002)"},{"key":"9053_CR27","first-page":"457","volume-title":"Proc. 14th Annual Conf. of the European Association for Computer Science Logic, LNCS 1862 (CSL\u201900)","author":"H. Ohsaki","year":"2000","unstructured":"Ohsaki, H., Middeldorp, A., Giesl, J.: Equational termination by semantic labeling. In: Proc. 14th Annual Conf. of the European Association for Computer Science Logic, LNCS 1862 (CSL\u201900), pp. 457\u2013471, Fischbachau\/Munich, Germany. Springer, Berlin Heidelberg New York (2000)"},{"key":"9053_CR28","volume-title":"Term rewriting systems. Cambridge Tracts in Theoretical Computer Science, vol. 55","author":"Terese","year":"2003","unstructured":"Terese. Term rewriting systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press, Cambridge, UK (2003)"},{"key":"9053_CR29","doi-asserted-by":"crossref","unstructured":"Thiemann, R., Giesl, J., Schneider-Kamp, P.: Improved modular termination proofs using dependency pairs. In: Proc. 2nd Int. Joint Conf. on Automated Reasoning, LNAI 3097 (IJCAR2004), pp. 75\u201390 (2004)","DOI":"10.1007\/978-3-540-25984-8_4"},{"key":"9053_CR30","doi-asserted-by":"crossref","unstructured":"Urbain, X.: Automated incremental termination proofs for hierarchically defined term rewriting systems. In: Proc. 10th Int. Joint Conf. on Automated Reasoning, LNAI 2083 (IJCAR\u201901), pp. 485\u2013498 (2001)","DOI":"10.1007\/3-540-45744-5_42"},{"key":"9053_CR31","unstructured":"Urbain, X.: Approche incr\u00e9mentale des Preuves automatiques de Termination. Ph.D. Thesis, Universit\u00e9 Paris-Sud, France (2002)"},{"issue":"4","key":"9053_CR32","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1007\/BF03177743","volume":"32","author":"X. Urbain","year":"2004","unstructured":"Urbain, X.: Modular & incremental automated termination proofs. J. Autom. Reason. 32(4), 315\u2013355 (2004)","journal-title":"J. Autom. Reason."},{"key":"9053_CR33","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1006\/jsco.1994.1003","volume":"17","author":"H. Zantema","year":"1994","unstructured":"Zantema, H.: Termination of term rewriting: Interpretation and type elimination. J. Symb. Comput. 17, 23\u201350 (1994)","journal-title":"J. Symb. Comput."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9053-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-006-9053-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9053-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T21:21:47Z","timestamp":1559251307000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-006-9053-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,12,2]]},"references-count":33,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2007,1,23]]}},"alternative-id":["9053"],"URL":"https:\/\/doi.org\/10.1007\/s10817-006-9053-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,12,2]]}}}