{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T20:04:46Z","timestamp":1742933086385,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031712937"},{"type":"electronic","value":"9783031712944"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-71294-4_11","type":"book-chapter","created":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T14:03:47Z","timestamp":1725631427000},"page":"185-201","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Proving Uniqueness of\u00a0Normal Forms w.r.t Reduction of\u00a0Term Rewriting Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0027-0759","authenticated-orcid":false,"given":"Takahito","family":"Aoto","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,9,7]]},"reference":[{"key":"11_CR1","unstructured":"Aoto, T., Toyama, Y.: Top-down labelling and modularity of term rewriting systems. Research Report IS-RR-96-0023F, School of Information Science, JAIST (1996)"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/BFb0027006","volume-title":"Algebraic and Logic Programming","author":"T Aoto","year":"1997","unstructured":"Aoto, T., Toyama, Y.: On composable properties of term rewriting systems. In: Hanus, M., Heering, J., Meinke, K. (eds.) ALP\/HOA -1997. LNCS, vol. 1298, pp. 114\u2013128. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0027006"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/978-3-030-29007-8_19","volume-title":"Frontiers of Combining Systems","author":"T Aoto","year":"2019","unstructured":"Aoto, T., Toyama, Y.: Automated proofs of unique normal forms w.r.t. conversion for term rewriting systems. In: Herzig, A., Popescu, A. (eds.) FroCoS 2019. LNCS (LNAI), vol. 11715, pp. 330\u2013347. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29007-8_19"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-02348-4_7","volume-title":"Rewriting Techniques and Applications","author":"T Aoto","year":"2009","unstructured":"Aoto, T., Yoshida, J., Toyama, Y.: Proving confluence of term rewriting systems automatically. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 93\u2013102. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02348-4_7"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)","DOI":"10.1017\/CBO9781139172752"},{"key":"11_CR6","doi-asserted-by":"publisher","unstructured":"Felgenhauer, B.: Deciding confluence and normal form properties of ground term rewrite systems efficiently. Logical Methods Comput. Sci. 14(4:7), 1\u201335 (2018). https:\/\/doi.org\/10.23638\/LMCS-14(4:7)2018","DOI":"10.23638\/LMCS-14"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-642-02348-4_5","volume-title":"Rewriting Techniques and Applications","author":"G Godoy","year":"2009","unstructured":"Godoy, G., Jacquemard, F.: Unique normalization for shallow TRS. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 63\u201377. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02348-4_5"},{"issue":"4","key":"11_CR8","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G Huet","year":"1980","unstructured":"Huet, G.: Confluent reductions: abstract properties and applications to term rewriting systems. J. ACM 27(4), 797\u2013821 (1980). https:\/\/doi.org\/10.1145\/322217.322230","journal-title":"J. ACM"},{"key":"11_CR9","doi-asserted-by":"publisher","unstructured":"Kahrs, S., Smith, C.: Non-$$\\omega $$-overlapping TRSs are UN. In: Proceedings of 1st FSCD. LIPIcs, vol.\u00a052, pp. 22:1\u201317. Schloss Dagstuhl (2016). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2016.22","DOI":"10.4230\/LIPIcs.FSCD.2016.22"},{"key":"11_CR10","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1006\/jsco.1996.0002","volume":"21","author":"R Kennaway","year":"1996","unstructured":"Kennaway, R., Klop, J.W., Sleep, R., de Vries, F.J.: Comparing curried and uncurried rewriting. J. Symb. Comput. 21, 15\u201339 (1996). https:\/\/doi.org\/10.1006\/jsco.1996.0002","journal-title":"J. Symb. Comput."},{"issue":"1","key":"11_CR11","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1006\/inco.2000.2888","volume":"164","author":"Z Khasidashvili","year":"2001","unstructured":"Khasidashvili, Z., Ogawa, M., van Oostrom, V.: Perpetuality and uniform normalization in orthogonal rewrite systems. Inf. Comput. 164(1), 118\u2013151 (2001). https:\/\/doi.org\/10.1006\/inco.2000.2888","journal-title":"Inf. Comput."},{"key":"11_CR12","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1006\/jsco.1996.0045","volume":"22","author":"M Marchiori","year":"1996","unstructured":"Marchiori, M.: On the modularity of normal forms in rewriting. J. Symb. Comput. 22, 143\u2013154 (1996). https:\/\/doi.org\/10.1006\/jsco.1996.0045","journal-title":"J. Symb. Comput."},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/3-540-51081-8_113","volume-title":"Rewriting Techniques and Applications","author":"A Middeldorp","year":"1989","unstructured":"Middeldorp, A.: Modular aspects of properties of term rewriting systems related to normal forms. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol. 355, pp. 263\u2013277. Springer, Heidelberg (1989). https:\/\/doi.org\/10.1007\/3-540-51081-8_113"},{"key":"11_CR14","doi-asserted-by":"publisher","unstructured":"Nagele, J., Felgenhauer, B., Middeldorp, A.: Improving automatic confluence analysis of rewrite systems by redundant rules. In: Proceedings of 26th RTA. LIPIcs, vol.\u00a036, pp. 257\u2013268. Schloss Dagstuhl (2015). https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2015.257","DOI":"10.4230\/LIPIcs.RTA.2015.257"},{"key":"11_CR15","doi-asserted-by":"publisher","unstructured":"Radcliffe, N., Moreas, L., Verma, R.: Uniqueness of normal forms for shallow term rewrite systems. ACM Trans. Comput. Logic 18(2), 17:1\u201317:20 (2017). https:\/\/doi.org\/10.1145\/3060144","DOI":"10.1145\/3060144"},{"issue":"2","key":"11_CR16","first-page":"15","volume":"14","author":"Y Sato","year":"2021","unstructured":"Sato, Y., Aoto, T.: Undecidability of some properties related to the uniqueness of normal forms for flat term rewiting systems. IPSJ Trans. Program. 14(2), 15\u201324 (2021). (in Japanese)","journal-title":"IPSJ Trans. Program."},{"issue":"1","key":"11_CR17","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1145\/7531.7534","volume":"34","author":"Y Toyama","year":"1987","unstructured":"Toyama, Y.: On the Church-Rosser property for the direct sum of term rewriting systems. J. ACM 34(1), 128\u2013143 (1987). https:\/\/doi.org\/10.1145\/7531.7534","journal-title":"J. ACM"},{"key":"11_CR18","unstructured":"Toyama, Y., Oyamaguchi, M.: Conditional linearization of non-duplicating term rewriting systems. IEICE Trans. Inf. Syst. E84-D(4), 439\u2013447 (2001)"},{"issue":"1","key":"11_CR19","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/S0304-3975(96)00173-9","volume":"175","author":"V van Oostrom","year":"1997","unstructured":"van Oostrom, V.: Developing developments. Theoret. Comput. Sci. 175(1), 159\u2013181 (1997). https:\/\/doi.org\/10.1016\/S0304-3975(96)00173-9","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"11_CR20","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1016\/S0019-3577(99)80012-3","volume":"10","author":"R de Vrijer","year":"1999","unstructured":"de Vrijer, R.: Conditional linearization. Indag. Math. 10(1), 145\u2013159 (1999). https:\/\/doi.org\/10.1016\/S0019-3577(99)80012-3","journal-title":"Indag. Math."},{"key":"11_CR21","doi-asserted-by":"publisher","unstructured":"Yamaguchi, M., Aoto, T.: A fast decision procedure for uniqueness of normal forms w.r.t. conversion of shallow term rewriting systems. In: Proceedings of 5th FSCD, LIPIcs, vol.\u00a0167, pp. 11:1\u201323. Schloss Dagstuhl (2020). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2020.11","DOI":"10.4230\/LIPIcs.FSCD.2020.11"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71294-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T14:05:25Z","timestamp":1725631525000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71294-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031712937","9783031712944"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71294-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"7 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"LOPSTR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Logic-Based Program Synthesis and Transformation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"lopstr2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/?page_id=63#lopstrppdp2024","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}