{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:00:23Z","timestamp":1750309223904,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,7,8]],"date-time":"2024-07-08T00:00:00Z","timestamp":1720396800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,7,8]]},"DOI":"10.1145\/3661814.3662081","type":"proceedings-article","created":{"date-parts":[[2024,6,21]],"date-time":"2024-06-21T12:30:12Z","timestamp":1718973012000},"page":"1-12","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Linear Termination is Undecidable"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5992-9517","authenticated-orcid":false,"given":"Fabian","family":"Mitterwallner","sequence":"first","affiliation":[{"name":"Computer Science, University of Innsbruck, Innsbruck, Austria"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7366-8464","authenticated-orcid":false,"given":"Aart","family":"Middeldorp","sequence":"additional","affiliation":[{"name":"Computer Science, University of Innsbruck, Innsbruck, Austria"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0323-8829","authenticated-orcid":false,"given":"Ren\u00e9","family":"Thiemann","sequence":"additional","affiliation":[{"name":"Computer Science, University of Innsbruck, Innsbruck, Austria"}]}],"member":"320","published-online":{"date-parts":[[2024,7,8]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00207-8"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2019.33"},{"key":"e_1_3_2_1_4_1","volume-title":"Diophantine Equations and the DPRM Theorem. Archive of Formal Proofs (June","author":"Bayer Jonas","year":"2022","unstructured":"Jonas Bayer, Marco David, Benedikt Stock, Abhik Pal, Yuri Matiyasevich, and Dierk Schleicher. 2022. Diophantine Equations and the DPRM Theorem. Archive of Formal Proofs (June 2022). https:\/\/isa-afp.org\/entries\/DPRM_Theorem.html, Formal proof development."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22438-6_11"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_9"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90030-X"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-07407-4_17"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90022-8"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(87)80022-6"},{"key":"e_1_3_2_1_11_1","volume-title":"Archive of Formal Proofs (September","author":"Eberl Manuel","year":"2018","unstructured":"Manuel Eberl. 2018. Symmetric Polynomials. Archive of Formal Proofs (September 2018). https:\/\/isa-afp.org\/entries\/Symmetric_Polynomials.html, Formal proof development."},{"key":"e_1_3_2_1_12_1","volume-title":"Factorization of Polynomials with Algebraic Coefficients. Archive of Formal Proofs (November","author":"Eberl Manuel","year":"2021","unstructured":"Manuel Eberl and Ren\u00e9 Thiemann. 2021. Factorization of Polynomials with Algebraic Coefficients. Archive of Formal Proofs (November 2021). https:\/\/isa-afp.org\/entries\/Factor_Algebraic_Polynomial.html, Formal proof development."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9087-9"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1996.0095"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2002.3120"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45127-7_10"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-51081-8_107"},{"key":"e_1_3_2_1_19_1","volume-title":"Bendix","author":"Knuth Donald E.","year":"1970","unstructured":"Donald E. Knuth and Peter B. Bendix. 1970. Simple Word Problems in Universal Algebras. In Computational Problems in Abstract Algebra, John Leech (Ed.). Pergamon Press, 263--297."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/1774732.1774738"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00021-X"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22438-6_29"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1051\/ita:2005029"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00200-005-0189-5"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75560-9_26"},{"key":"e_1_3_2_1_27_1","first-page":"354","article-title":"Enumerable Sets are Diophantine (translated from Russian)","volume":"11","author":"Matijasevic Yuri Y.","year":"1970","unstructured":"Yuri Y. Matijasevic. 1970. Enumerable Sets are Diophantine (translated from Russian). In Soviet Mathematics Doklady, Vol. 11. 354--358.","journal-title":"Soviet Mathematics Doklady"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561469"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2004.09.016"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01225647"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2022.27"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(3:22)2014"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_1_34_1","volume-title":"A Formalization of Knuth-Bendix Orders. Archive of Formal Proofs (May","author":"Sternagel Christian","year":"2020","unstructured":"Christian Sternagel and Ren\u00e9 Thiemann. 2020. A Formalization of Knuth-Bendix Orders. Archive of Formal Proofs (May 2020). https:\/\/isa-afp.org\/entries\/Knuth_Bendix_Order.html, Formal proof development."},{"key":"e_1_3_2_1_35_1","volume-title":"Executable Multivariate Polynomials. Archive of Formal Proofs (August","author":"Sternagel Christian","year":"2010","unstructured":"Christian Sternagel, Ren\u00e9 Thiemann, Alexander Maletzky, Fabian Immler, Florian Haftmann, Andreas Lochbihler, and Alexander Bentkamp. 2010. Executable Multivariate Polynomials. Archive of Formal Proofs (August 2010). https:\/\/isa-afp.org\/entries\/Polynomials.html, Formal proof development."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1525\/9780520348097"},{"key":"e_1_3_2_1_37_1","volume-title":"Undecidability Results on Orienting Single Rewrite Rules. Archive of Formal Proofs (April","author":"Thiemann Ren\u00e9","year":"2024","unstructured":"Ren\u00e9 Thiemann, Fabian Mitterwallner, and Aart Middeldorp. 2024. Undecidability Results on Orienting Single Rewrite Rules. Archive of Formal Proofs (April 2024). https:\/\/isa-afp.org\/entries\/Orient_Rewrite_Rule_Undecidable.html, Formal proof development."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28717-6_33"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1994.1003"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1995.1037"},{"key":"e_1_3_2_1_41_1","first-page":"181","article-title":"Termination. In Term Rewriting Systems. Cambridge University Press","volume":"6","author":"Zantema Hans","year":"2003","unstructured":"Hans Zantema. 2003. Termination. In Term Rewriting Systems. Cambridge University Press, Chapter 6, 181--259.","journal-title":"Chapter"}],"event":{"name":"LICS '24: 39th Annual ACM\/IEEE Symposium on Logic in Computer Science","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","IEEE Computer Society","EACSL"],"location":"Tallinn Estonia","acronym":"LICS '24"},"container-title":["Proceedings of the 39th Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3661814.3662081","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3661814.3662081","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T23:44:08Z","timestamp":1750290248000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3661814.3662081"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,8]]},"references-count":39,"alternative-id":["10.1145\/3661814.3662081","10.1145\/3661814"],"URL":"https:\/\/doi.org\/10.1145\/3661814.3662081","relation":{},"subject":[],"published":{"date-parts":[[2024,7,8]]},"assertion":[{"value":"2024-07-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}