{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,26]],"date-time":"2025-08-26T07:05:10Z","timestamp":1756191910036},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540735946"},{"type":"electronic","value":"9783540735953"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73595-3_17","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T09:31:33Z","timestamp":1188466293000},"page":"247-262","source":"Crossref","is-referenced-by-count":6,"title":["On the Normalization and Unique Normalization Properties of Term Rewrite Systems"],"prefix":"10.1007","author":[{"given":"Guillem","family":"Godoy","sequence":"first","affiliation":[]},{"given":"Sophie","family":"Tison","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Bachmair, L.: Canonical Equational Proofs. Birkh\u00e4user, Boston (1991)","DOI":"10.1007\/978-1-4684-7118-2"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Bogaert, B., Tison, S.: Equality and disequality constraints on direct subterms in tree automata. In: International Symposium on Theoretical Aspects of Computeter Science, pp. 161\u2013171 (1992)","DOI":"10.1007\/3-540-55210-3_181"},{"key":"17_CR3","unstructured":"Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (1997), Available on http:\/\/www.grappa.univ-lille3.fr\/tata"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science (Vol.\u00a0B: Formal Models and Semantics), pp. 243\u2013320, Amsterdam, North-Holland (1990)","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"17_CR5","unstructured":"Durand, I.: Call by need computations in orthogonal term rewriting systems, 07, Habilitation diriger des recherches de l\u2019universit\u00e9 de Bordeaux (2005)"},{"issue":"1\/2","key":"17_CR6","doi-asserted-by":"crossref","first-page":"157","DOI":"10.3233\/FI-1995-24127","volume":"24","author":"R. Gilleron","year":"1995","unstructured":"Gilleron, R., Tison, S.: Regular tree languages and rewrite systems. Fundam. Inform.\u00a024(1\/2), 157\u2013174 (1995)","journal-title":"Fundam. Inform."},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/11538363_37","volume-title":"Computer Science Logic","author":"G. Godoy","year":"2005","unstructured":"Godoy, G., Tiwari, A.: Confluence of shallow right-linear rewrite systems. In: Luke, C.-H. (ed.) CSL 2005. LNCS, vol.\u00a03634, pp. 541\u2013556. Springer, Heidelberg (2005)"},{"key":"17_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1007\/11532231_12","volume-title":"Automated Deduction \u2013 CADE-20","author":"G. Godoy","year":"2005","unstructured":"Godoy, G., Tiwari, A.: Termination of rewrite systems with shallow right-linear, collapsing, and right-ground rules. In: Nieuwenhuis, R. (ed.) Automated Deduction \u2013 CADE-20. LNCS (LNAI), vol.\u00a03632, pp. 164\u2013176. Springer, Heidelberg (2005)"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/3-540-36494-3_9","volume-title":"STACS 2003","author":"G. Godoy","year":"2003","unstructured":"Godoy, G., Tiwari, A., Verma, R.: On the confluence of linear shallow term rewrite systems. In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol.\u00a02607, pp. 85\u201396. Springer, Heidelberg (2003)"},{"issue":"1-3","key":"17_CR10","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1016\/j.apal.2004.04.005","volume":"130","author":"G. Godoy","year":"2004","unstructured":"Godoy, G., Tiwari, A., Verma, R.: Deciding confluence of certain term rewriting systems in polynomial time. Annals of Pure and Applied Logic\u00a0130(1-3), 33\u201359 (2004)","journal-title":"Annals of Pure and Applied Logic"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Jacquemard, F.: Decidable approximations of term rewriting systems. In: Rewriting Techniques and Applications, 7th International Conference, pp. 362\u2013376 (1996)","DOI":"10.1007\/3-540-61464-8_65"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/3-540-56868-9_3","volume-title":"Rewriting Techniques and Applications","author":"J. Levy","year":"1993","unstructured":"Levy, J., Agusti, J.: Bi-rewriting, a term rewriting technique for monotone order relations. In: Kirchner, C. (ed.) Rewriting Techniques and Applications. LNCS, vol.\u00a0690, pp. 17\u201331. Springer, Heidelberg (1993)"},{"issue":"2","key":"17_CR13","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1006\/inco.2002.3157","volume":"178","author":"T. Nagaya","year":"2002","unstructured":"Nagaya, T., Toyama, Y.: Decidability for left-linear growing term rewriting systems. Inf. Comput.\u00a0178(2), 499\u2013514 (2002)","journal-title":"Inf. Comput."},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/3-540-45294-X_28","volume-title":"FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science","author":"A. Tiwari","year":"2001","unstructured":"Tiwari, A.: Rewrite closure for ground and cancellative AC theories. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science. LNCS, vol.\u00a02245, pp. 334\u2013346. Springer, Heidelberg (2001)"},{"key":"17_CR15","unstructured":"Tiwari, A.: On the combination of equational and rewrite theories induced by certain term rewrite systems. Menlo Park, CA 94025 (2002), Available at: www.csl.sri.com\/~tiwari\/combinationER.ps"},{"issue":"1","key":"17_CR16","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/1042038.1042042","volume":"6","author":"R. Verma","year":"2005","unstructured":"Verma, R., Hayrapetyan, A.: A new decidability technique for ground term rewriting systems. ACM Trans. Comput. Log.\u00a06(1), 102\u2013123 (2005)","journal-title":"ACM Trans. Comput. Log."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-21"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73595-3_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:16:21Z","timestamp":1605762981000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735946","9783540735953"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}