{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:03:40Z","timestamp":1725516220516},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540705888"},{"type":"electronic","value":"9783540705901"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70590-1_23","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T12:07:43Z","timestamp":1218542863000},"page":"336-350","source":"Crossref","is-referenced-by-count":10,"title":["Root-Labeling"],"prefix":"10.1007","author":[{"given":"Christian","family":"Sternagel","sequence":"first","affiliation":[]},{"given":"Aart","family":"Middeldorp","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","doi-asserted-by":"publisher","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. Theoretical Computer Science\u00a0236, 133\u2013178 (2000)","journal-title":"Theoretical Computer Science"},{"key":"23_CR2","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, Cambridge (1998)"},{"key":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"23_CR4","unstructured":"Endrullis, J.: Jambox (2005), http:\/\/joerg.endrullis.de"},{"key":"23_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"574","DOI":"10.1007\/11814771_47","volume-title":"Automated Reasoning","author":"J. Endrullis","year":"2006","unstructured":"Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 574\u2013588. Springer, Heidelberg (2006)"},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-540-72788-0_33","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"C. Fuhs","year":"2007","unstructured":"Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 340\u2013354. Springer, Heidelberg (2007)"},{"key":"23_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11814771_24","volume-title":"Automated Reasoning","author":"J. Giesl","year":"2006","unstructured":"Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 281\u2013286. Springer, Heidelberg (2006)"},{"key":"23_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/978-3-540-32275-7_21","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J. Giesl","year":"2005","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework: Combining techniques for automated termination proofs. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 301\u2013331. Springer, Heidelberg (2005)"},{"issue":"3","key":"23_CR9","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/s10817-006-9057-7","volume":"37","author":"J. Giesl","year":"2006","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. Journal of Automated Reasoning\u00a037(3), 155\u2013203 (2006)","journal-title":"Journal of Automated Reasoning"},{"issue":"1,2","key":"23_CR10","doi-asserted-by":"publisher","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. Information and Computation\u00a0199(1,2), 172\u2013199 (2005)","journal-title":"Information and Computation"},{"key":"23_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/11805618_24","volume-title":"Term Rewriting and Applications","author":"N. Hirokawa","year":"2006","unstructured":"Hirokawa, N., Middeldorp, A.: Predictive labeling. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 313\u2013327. Springer, Heidelberg (2006)"},{"key":"23_CR12","unstructured":"Hofbauer, D.: MultumNonMulta (2006), www.theory.informatik.uni-kassel.de\/~dieter\/multum\/"},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/11805618_19","volume-title":"Term Rewriting and Applications","author":"A. Koprowski","year":"2006","unstructured":"Koprowski, A.: TPA: Termination proved automatically. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 257\u2013266. Springer, Heidelberg (2006)"},{"key":"23_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/978-3-540-73595-3_31","volume-title":"Automated Deduction \u2013 CADE-21","author":"A. Koprowski","year":"2007","unstructured":"Koprowski, A., Middeldorp, A.: Predictive labeling with dependency pairs using SAT. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 410\u2013425. Springer, Heidelberg (2007)"},{"key":"23_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/11814771_30","volume-title":"Automated Reasoning","author":"A. Koprowski","year":"2006","unstructured":"Koprowski, A., Zantema, H.: Recursive path ordering for infinite labelled rewrite systems. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 332\u2013346. Springer, Heidelberg (2006)"},{"key":"23_CR16","unstructured":"Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean termination tool 2 (2007), http:\/\/colo6-c703.uibk.ac.at\/ttt2"},{"key":"23_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1007\/3-540-61511-3_101","volume-title":"Automated Deduction - Cade-13","author":"A. Middeldorp","year":"1996","unstructured":"Middeldorp, A., Ohsaki, H., Zantema, H.: Transforming termination by self-labelling. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol.\u00a01104, pp. 373\u2013386. Springer, Heidelberg (1996)"},{"key":"23_CR18","series-title":"Cambridge Tracts in Theoretical Computer Science","volume-title":"Term Rewriting Systems","author":"Terese","year":"2003","unstructured":"Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol.\u00a055. Cambridge University Press, Cambridge (2003)"},{"key":"23_CR19","unstructured":"Thiemann, R.: The DP Framework for Proving Termination of Term Rewriting. PhD thesis, RWTH Aachen, Technical report AIB-2007-17 (2007)"},{"key":"23_CR20","doi-asserted-by":"crossref","unstructured":"Thiemann, R., Middeldorp, A.: Innermost termination of rewrite systems by labeling. In: Giesel, J. (ed.) WRS 2007. ENTCS, vol.\u00a0204, pp. 3\u201319 (2008)","DOI":"10.1016\/j.entcs.2008.03.050"},{"key":"23_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1007\/BFb0055079","volume-title":"Automata, Languages and Programming","author":"H. Touzet","year":"1998","unstructured":"Touzet, H.: A complex example of a simplifying rewrite system. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443, pp. 507\u2013517. Springer, Heidelberg (1998)"},{"key":"23_CR22","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/0020-0190(87)90122-0","volume":"25","author":"Y. Toyama","year":"1987","unstructured":"Toyama, Y.: Counterexamples to the termination for the direct sum of term rewriting systems. Information Processing Letters\u00a025, 141\u2013143 (1987)","journal-title":"Information Processing Letters"},{"key":"23_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/978-3-540-25979-4_6","volume-title":"Rewriting Techniques and Applications","author":"J. Waldmann","year":"2004","unstructured":"Waldmann, J.: Matchbox: A tool for match-bounded string rewriting. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol.\u00a03091, pp. 85\u201394. Springer, Heidelberg (2004)"},{"key":"23_CR24","doi-asserted-by":"crossref","first-page":"89","DOI":"10.3233\/FI-1995-24124","volume":"24","author":"H. Zantema","year":"1995","unstructured":"Zantema, H.: Termination of term rewriting by semantic labelling. Fundamenta Informaticae\u00a024, 89\u2013105 (1995)","journal-title":"Fundamenta Informaticae"},{"key":"23_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/978-3-540-25979-4_7","volume-title":"Rewriting Techniques and Applications","author":"H. Zantema","year":"2004","unstructured":"Zantema, H.: TORPA: Termination of rewriting proved automatically. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol.\u00a03091, pp. 95\u2013104. Springer, Heidelberg (2004)"},{"key":"23_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-540-73449-9_30","volume-title":"Term Rewriting and Applications","author":"H. Zantema","year":"2007","unstructured":"Zantema, H., Waldmann, J.: Termination by quasi-periodic interpretations. In: Baader, F. (ed.) RTA 2007. LNCS, vol.\u00a04533, pp. 404\u2013418. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70590-1_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T00:08:20Z","timestamp":1605744500000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70590-1_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540705888","9783540705901"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70590-1_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}