{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T03:09:02Z","timestamp":1761620942389},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540371878"},{"type":"electronic","value":"9783540371885"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814771_30","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T15:44:21Z","timestamp":1160063061000},"page":"332-346","source":"Crossref","is-referenced-by-count":6,"title":["Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems"],"prefix":"10.1007","author":[{"given":"Adam","family":"Koprowski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hans","family":"Zantema","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"30_CR1","unstructured":"The termination competition, http:\/\/www.lri.fr\/~marche\/termination-competition"},{"key":"30_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)"},{"issue":"2","key":"30_CR3","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1016\/0167-6423(87)90030-X","volume":"9","author":"A.B. Cherifa","year":"1987","unstructured":"Cherifa, A.B., Lescanne, P.: Termination of rewriting systems by polynomial interpretations and its implementation. Sci. Comput. Program.\u00a09(2), 137\u2013159 (1987)","journal-title":"Sci. Comput. Program."},{"key":"30_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/3-540-55808-X_19","volume-title":"Mathematical Foundations of Computer Science 1992","author":"P.-L. Curien","year":"1992","unstructured":"Curien, P.-L., Hardin, T., R\u00edos, A.: Strong normalization of substitutions. In: Havel, I.M., Koubek, V. (eds.) MFCS 1992. LNCS, vol.\u00a0629, pp. 209\u2013217. Springer, Heidelberg (1992)"},{"key":"30_CR5","doi-asserted-by":"publisher","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. Comput. Sci.\u00a017, 279\u2013301 (1982)","journal-title":"Theor. Comput. Sci."},{"key":"30_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-540-25979-4_15","volume-title":"Rewriting Techniques and Applications","author":"J. Giesl","year":"2004","unstructured":"Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Automated termination proofs with AProVE. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol.\u00a03091, pp. 210\u2013220. Springer, Heidelberg (2004)"},{"issue":"2-3","key":"30_CR7","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1016\/0304-3975(86)90035-6","volume":"46","author":"T. Hardin","year":"1986","unstructured":"Hardin, T., Laville, A.: Proof of termination of the rewriting system SUBST on CCL. Theor. Comput. Sci.\u00a046(2-3), 305\u2013312 (1986)","journal-title":"Theor. Comput. Sci."},{"key":"30_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 17th Conference on Rewriting Techniques and Applications (RTA)","author":"N. Hirokawa","year":"2006","unstructured":"Hirokawa, N., Middeldorp, A.: Predictive labeling. In: Pfenning, F. (ed.) Proceedings of the 17th Conference on Rewriting Techniques and Applications (RTA). LNCS, Springer, Heidelberg (2006)"},{"issue":"1","key":"30_CR9","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1023\/A:1005983105493","volume":"21","author":"H. Hong","year":"1998","unstructured":"Hong, H., Jakus, D.: Testing Positiveness of Polynomials. J. Autom. Reasoning\u00a021(1), 23\u201338 (1998)","journal-title":"J. Autom. Reasoning"},{"key":"30_CR10","doi-asserted-by":"crossref","unstructured":"Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: Computational Problems in Abstract Algebra, pp. 263\u2013297 (1970)","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"30_CR11","doi-asserted-by":"crossref","unstructured":"Koprowski, A., Zantema, H.: Recursive Path Ordering for Infinite Labelled Rewrite Systems. Technical Report CS-Report 06-17, Eindhoven Univ. of Tech (April 2006)","DOI":"10.1007\/11814771_30"},{"issue":"1\/2","key":"30_CR12","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(1\/2), 89\u2013105 (1995)","journal-title":"Fundamenta Informaticae"},{"key":"30_CR13","first-page":"181","volume-title":"Cambridge Tracts in TCS, ch. 6","author":"H. Zantema","year":"2003","unstructured":"Zantema, H.: Term Rewriting Systems. In: Cambridge Tracts in TCS, ch. 6, vol.\u00a055, pp. 181\u2013259. Cambridge University Press, Cambridge (2003)"},{"key":"30_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,18]],"date-time":"2020-04-18T12:35:45Z","timestamp":1587213345000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/11814771_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}