{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,20]],"date-time":"2026-07-20T19:06:20Z","timestamp":1784574380126,"version":"3.55.0"},"reference-count":58,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2023,4,25]],"date-time":"2023-04-25T00:00:00Z","timestamp":1682380800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,25]],"date-time":"2023-04-25T00:00:00Z","timestamp":1682380800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-2006363"],"award-info":[{"award-number":["CCF-2006363"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2023,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We explore the Collatz conjecture and its variants through the lens of termination of string rewriting. We construct a rewriting system that simulates the iterated application of the Collatz function on strings corresponding to mixed binary\u2013ternary representations of positive integers. We prove that the termination of this rewriting system is equivalent to the Collatz conjecture. We also prove that a previously studied rewriting system that simulates the Collatz function using unary representations does not admit termination proofs via natural matrix interpretations, even when used in conjunction with dependency pairs. To show the feasibility of our approach in proving mathematically interesting statements, we implement a minimal termination prover that uses natural\/arctic matrix interpretations and we find automated proofs of nontrivial weakenings of the Collatz conjecture. Although we do not succeed in proving the Collatz conjecture, we believe that the ideas here represent an interesting new approach.<\/jats:p>","DOI":"10.1007\/s10817-022-09658-8","type":"journal-article","created":{"date-parts":[[2023,4,25]],"date-time":"2023-04-25T04:02:15Z","timestamp":1682395335000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["An Automated Approach to the Collatz Conjecture"],"prefix":"10.1007","volume":"67","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4255-9748","authenticated-orcid":false,"given":"Emre","family":"Yolcu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Scott","family":"Aaronson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5587-8801","authenticated-orcid":false,"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,4,25]]},"reference":[{"key":"9658_CR1","doi-asserted-by":"publisher","DOI":"10.1090\/mbk\/078","volume-title":"The Ultimate Challenge: The $$3x+1$$ Problem","author":"JC Lagarias","year":"2010","unstructured":"Lagarias, J.C.: The Ultimate Challenge: The $$3x+1$$ Problem. American Mathematical Society, Providence (2010)"},{"key":"9658_CR2","unstructured":"Lagarias, J.C.: The $$3x+1$$ Problem: An Annotated Bibliography (1963\u20131999). arXiv:math\/0309224 (2011)"},{"key":"9658_CR3","unstructured":"Lagarias, J.C.: The $$3x+1$$ Problem: An Annotated Bibliography, II (2000\u20132009). arXiv:math\/0608208 (2012)"},{"key":"9658_CR4","unstructured":"Tao, T.: Almost All Orbits of the Collatz Map Attain Almost Bounded Values. arXiv:1909.03562 (2020)"},{"issue":"3","key":"9658_CR5","doi-asserted-by":"publisher","first-page":"2681","DOI":"10.1007\/s11227-020-03368-x","volume":"77","author":"D Barina","year":"2021","unstructured":"Barina, D.: Convergence verification of the Collatz problem. The Journal of Supercomputing 77(3), 2681\u20132688 (2021). https:\/\/doi.org\/10.1007\/s11227-020-03368-x","journal-title":"The Journal of Supercomputing"},{"issue":"1","key":"9658_CR6","doi-asserted-by":"publisher","first-page":"3","DOI":"10.2307\/2322189","volume":"92","author":"JC Lagarias","year":"1985","unstructured":"Lagarias, J.C.: The $$3x+1$$ problem and its generalizations. The American Mathematical Monthly 92(1), 3\u201323 (1985). https:\/\/doi.org\/10.2307\/2322189","journal-title":"The American Mathematical Monthly"},{"key":"9658_CR7","unstructured":"Conway, J.H.: Unpredictable iterations. In: Proceedings of the Number Theory Conference (University of Colorado, Boulder, Colorado), pp. 49\u201352 (1972)"},{"key":"9658_CR8","doi-asserted-by":"publisher","unstructured":"Kurtz, S.A., Simon, J.: The undecidability of the generalized Collatz problem. In: Proceedings of the 4th International Conference on Theory and Applications of Models of Computation (TAMC). Lecture Notes in Computer Science, pp. 542\u2013553. Springer, New York (2007). https:\/\/doi.org\/10.1007\/978-3-540-72504-6_49","DOI":"10.1007\/978-3-540-72504-6_49"},{"key":"9658_CR9","doi-asserted-by":"publisher","unstructured":"Hofbauer, D., Waldmann, J.: Termination of string rewriting with matrix interpretations. In: Proceedings of the 17th International Conference on Rewriting Techniques and Applications (RTA). Lecture Notes in Computer Science, pp. 328\u2013342. Springer, New York (2006). https:\/\/doi.org\/10.1007\/11805618_25","DOI":"10.1007\/11805618_25"},{"issue":"2","key":"9658_CR10","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s10817-007-9087-9","volume":"40","author":"J Endrullis","year":"2008","unstructured":"Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. Journal of Automated Reasoning 40(2), 195\u2013220 (2008). https:\/\/doi.org\/10.1007\/s10817-007-9087-9","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"9658_CR11","first-page":"357","volume":"19","author":"A Koprowski","year":"2009","unstructured":"Koprowski, A., Waldmann, J.: Max\/plus tree automata for termination of term rewriting. Acta Cybernetica 19(2), 357\u2013392 (2009)","journal-title":"Acta Cybernetica"},{"key":"9658_CR12","doi-asserted-by":"publisher","unstructured":"Sternagel, C., Thiemann, R.: Formalizing monotone algebras for certification of termination and complexity proofs. In: Proceedings of the 25th International Conference on Rewriting Techniques and Applications (RTA). Lecture Notes in Computer Science, pp. 441\u2013455. Springer, New York (2014). https:\/\/doi.org\/10.1007\/978-3-319-08918-8_30","DOI":"10.1007\/978-3-319-08918-8_30"},{"issue":"2","key":"9658_CR13","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/s10817-005-6545-0","volume":"34","author":"H Zantema","year":"2005","unstructured":"Zantema, H.: Termination of string rewriting proved automatically. Journal of Automated Reasoning 34(2), 105\u2013139 (2005). https:\/\/doi.org\/10.1007\/s10817-005-6545-0","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"9658_CR14","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 236(1), 133\u2013178 (2000). https:\/\/doi.org\/10.1016\/S0304-3975(99)00207-8","journal-title":"Theoretical Computer Science"},{"issue":"5","key":"9658_CR15","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JP Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers 48(5), 506\u2013521 (1999). https:\/\/doi.org\/10.1109\/12.769433","journal-title":"IEEE Transactions on Computers"},{"key":"9658_CR16","doi-asserted-by":"publisher","unstructured":"Yolcu, E., Aaronson, S., Heule, M.J.H.: An automated approach to the Collatz conjecture. In: Proceedings of the 28th Conference on Automated Deduction (CADE). Lecture Notes in Computer Science, pp. 468\u2013484. Springer, New York (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_27","DOI":"10.1007\/978-3-030-79876-5_27"},{"key":"9658_CR17","doi-asserted-by":"publisher","unstructured":"Book, R.V., Otto, F.: String-Rewriting Systems. Springer, New York (1993). https:\/\/doi.org\/10.1007\/978-1-4613-9771-7","DOI":"10.1007\/978-1-4613-9771-7"},{"key":"9658_CR18","doi-asserted-by":"publisher","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998). https:\/\/doi.org\/10.1017\/CBO9781139172752","DOI":"10.1017\/CBO9781139172752"},{"issue":"1","key":"9658_CR19","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1006\/jsco.1994.1003","volume":"17","author":"H Zantema","year":"1994","unstructured":"Zantema, H.: Termination of term rewriting: Interpretation and type elimination. Journal of Symbolic Computation 17(1), 23\u201350 (1994). https:\/\/doi.org\/10.1006\/jsco.1994.1003","journal-title":"Journal of Symbolic Computation"},{"issue":"1","key":"9658_CR20","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10817-016-9388-y","volume":"58","author":"J Giesl","year":"2017","unstructured":"Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Hensel, J., Otto, C., Pl\u00fccker, M., Schneider-Kamp, P., Str\u00f6der, T., Swiderski, S., Thiemann, R.: Analyzing program termination and complexity automatically with AProVE. Journal of Automated Reasoning 58(1), 3\u201331 (2017). https:\/\/doi.org\/10.1007\/s10817-016-9388-y","journal-title":"Journal of Automated Reasoning"},{"key":"9658_CR21","doi-asserted-by":"publisher","unstructured":"Waldmann, J.: Matchbox: A tool for match-bounded string rewriting. In: Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA). Lecture Notes in Computer Science, pp. 85\u201394. Springer, New York (2004). https:\/\/doi.org\/10.1007\/978-3-540-25979-4_6","DOI":"10.1007\/978-3-540-25979-4_6"},{"key":"9658_CR22","doi-asserted-by":"publisher","unstructured":"Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean Termination Tool 2. In: Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA). Lecture Notes in Computer Science, pp. 295\u2013304. Springer, New York (2009). https:\/\/doi.org\/10.1007\/978-3-642-02348-4_21","DOI":"10.1007\/978-3-642-02348-4_21"},{"key":"9658_CR23","doi-asserted-by":"publisher","unstructured":"Courtieu, P., Gbedo, G., Pons, O.: Improved matrix interpretation. In: Proceedings of the 36th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM). Lecture Notes in Computer Science, pp. 283\u2013295. Springer, New York (2010). https:\/\/doi.org\/10.1007\/978-3-642-11266-9_24","DOI":"10.1007\/978-3-642-11266-9_24"},{"key":"9658_CR24","doi-asserted-by":"publisher","unstructured":"rn Neurauter, F., Middeldorp, A.: Revisiting matrix interpretations for proving termination of term rewriting. In: Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA). Leibniz International Proceedings in Informatics, pp. 251\u2013266. Schloss Dagstuhl, Wadern (2011). https:\/\/doi.org\/10.4230\/LIPIcs.RTA.2011.251","DOI":"10.4230\/LIPIcs.RTA.2011.251"},{"issue":"4","key":"9658_CR25","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1103\/PhysRevLett.59.381","volume":"59","author":"P Bak","year":"1987","unstructured":"Bak, P., Tang, C., Wiesenfeld, K.: Self-organized criticality: An explanation of the $$1\/f$$ noise. Physical Review Letters 59(4), 381\u2013384 (1987). https:\/\/doi.org\/10.1103\/PhysRevLett.59.381","journal-title":"Physical Review Letters"},{"issue":"3","key":"9658_CR26","doi-asserted-by":"publisher","first-page":"172","DOI":"10.2307\/2689917","volume":"58","author":"DA Rawsthorne","year":"1985","unstructured":"Rawsthorne, D.A.: Imitation of an iteration. Mathematics Magazine 58(3), 172\u2013176 (1985). https:\/\/doi.org\/10.2307\/2689917","journal-title":"Mathematics Magazine"},{"issue":"1","key":"9658_CR27","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/BF03023011","volume":"7","author":"S Wagon","year":"1985","unstructured":"Wagon, S.: The Collatz problem. The Mathematical Intelligencer 7(1), 72\u201376 (1985). https:\/\/doi.org\/10.1007\/BF03023011","journal-title":"The Mathematical Intelligencer"},{"issue":"1","key":"9658_CR28","doi-asserted-by":"publisher","first-page":"43","DOI":"10.4064\/aa-55-1-43-57","volume":"55","author":"RN Buttsworth","year":"1990","unstructured":"Buttsworth, R.N., Matthews, K.R.: On some Markov matrices arising from the generalized Collatz mapping. Acta Arithmetica 55(1), 43\u201357 (1990). https:\/\/doi.org\/10.4064\/aa-55-1-43-57","journal-title":"Acta Arithmetica"},{"key":"9658_CR29","doi-asserted-by":"publisher","unstructured":"Ka\u0161\u010d\u00e1k, F.: Small universal one-state linear operator algorithm. In: Proceedings of the 17th International Symposium on Mathematical Foundations of Computer Science (MFCS). Lecture Notes in Computer Science, pp. 327\u2013335. Springer, New York (1992). https:\/\/doi.org\/10.1007\/3-540-55808-X_31","DOI":"10.1007\/3-540-55808-X_31"},{"issue":"3","key":"9658_CR30","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1016\/j.aam.2006.08.003","volume":"39","author":"S Kohl","year":"2007","unstructured":"Kohl, S.: Wildness of iteration of certain residue-class-wise affine mappings. Advances in Applied Mathematics 39(3), 322\u2013328 (2007). https:\/\/doi.org\/10.1016\/j.aam.2006.08.003","journal-title":"Advances in Applied Mathematics"},{"key":"9658_CR31","doi-asserted-by":"publisher","unstructured":"Michel, P.: Problems in number theory from busy beaver competition. Logical Methods in Computer Science 11(4:10), (2015). https:\/\/doi.org\/10.2168\/LMCS-11(4:10)2015","DOI":"10.2168\/LMCS-11(4:10)2015"},{"key":"9658_CR32","doi-asserted-by":"publisher","unstructured":"Reutenauer, C., Berstel, J.: Noncommutative Rational Series with Applications. Cambridge University Press, Cambridge (2010). https:\/\/doi.org\/10.1017\/CBO9780511760860","DOI":"10.1017\/CBO9780511760860"},{"issue":"3","key":"9658_CR33","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/0304-3975(76)90084-0","volume":"2","author":"M Soittola","year":"1976","unstructured":"Soittola, M.: Positive rational sequences. Theoretical Computer Science 2(3), 317\u2013322 (1976). https:\/\/doi.org\/10.1016\/0304-3975(76)90084-0","journal-title":"Theoretical Computer Science"},{"key":"9658_CR34","first-page":"121","volume":"14","author":"G Cantor","year":"1869","unstructured":"Cantor, G.: \u00dcber einfache zahlensysteme. Zeitschrift f\u00fcr Mathematik und Physik 14, 121\u2013128 (1869)","journal-title":"Zeitschrift f\u00fcr Mathematik und Physik"},{"key":"9658_CR35","doi-asserted-by":"publisher","unstructured":"Sabel, D., Zantema, H.: Termination of cycle rewriting by transformation and matrix interpretation. Logical Methods in Computer Science 13(1:11), (2017). https:\/\/doi.org\/10.23638\/LMCS-13(1:11)2017","DOI":"10.23638\/LMCS-13(1:11)2017"},{"issue":"3","key":"9658_CR36","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 37(3), 155\u2013203 (2006). https:\/\/doi.org\/10.1007\/s10817-006-9057-7","journal-title":"Journal of Automated Reasoning"},{"key":"9658_CR37","doi-asserted-by":"publisher","unstructured":"Farkas, H.M.: Variants of the $$3N+1$$ conjecture and multiplicative semigroups. In: Geometry, Spectral Theory, Groups, and Dynamics. Contemporary Mathematics, pp. 121\u2013127. American Mathematical Society, Providence (2005). https:\/\/doi.org\/10.1090\/conm\/387\/07238","DOI":"10.1090\/conm\/387\/07238"},{"key":"9658_CR38","doi-asserted-by":"publisher","unstructured":"Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations. In: In: Proceedings of the 3rd International Conference on Rewriting Techniques and Applications (RTA). Lecture Notes in Computer Science, pp. 167\u2013177. Springer, New York (1989). https:\/\/doi.org\/10.1007\/3-540-51081-8_107","DOI":"10.1007\/3-540-51081-8_107"},{"key":"9658_CR39","doi-asserted-by":"publisher","unstructured":"Denend, M.: Challenging variants of the Collatz conjecture. Master\u2019s thesis, University of Texas at Austin (2018). https:\/\/doi.org\/10.26153\/tsw\/1559","DOI":"10.26153\/tsw\/1559"},{"issue":"242","key":"9658_CR40","doi-asserted-by":"publisher","first-page":"1035","DOI":"10.1090\/S0025-5718-02-01425-4","volume":"72","author":"D Applegate","year":"2003","unstructured":"Applegate, D., Lagarias, J.C.: Lower bounds for the total stopping time of $$3x+1$$ iterates. Mathematics of Computation 72(242), 1035\u20131049 (2003). https:\/\/doi.org\/10.1090\/S0025-5718-02-01425-4","journal-title":"Mathematics of Computation"},{"key":"9658_CR41","doi-asserted-by":"publisher","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing (SAT). Lecture Notes in Computer Science, pp. 502\u2013518. Springer, New York (2004). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"9658_CR42","doi-asserted-by":"publisher","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference (DAC), pp. 530\u2013535. Association for Computing Machinery, New York (2001). https:\/\/doi.org\/10.1145\/378239.379017","DOI":"10.1145\/378239.379017"},{"key":"9658_CR43","doi-asserted-by":"publisher","unstructured":"Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisfiability solvers. In: Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT). Lecture Notes in Computer Science, pp. 294\u2013299. Springer, New York (2007). https:\/\/doi.org\/10.1007\/978-3-540-72788-0_28","DOI":"10.1007\/978-3-540-72788-0_28"},{"issue":"2","key":"9658_CR44","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/s10601-008-9061-0","volume":"14","author":"N Tamura","year":"2009","unstructured":"Tamura, N., Taga, A., Kitagawa, S., Banbara, M.: Compiling finite linear CSP into SAT. Constraints 14(2), 254\u2013272 (2009). https:\/\/doi.org\/10.1007\/s10601-008-9061-0","journal-title":"Constraints"},{"key":"9658_CR45","doi-asserted-by":"publisher","unstructured":"Petke, J., Jeavons, P.: The order encoding: From tractable CSP to tractable SAT. In: Proceedings of the 14th International Conference on Theory and Applications of Satisfiability Testing (SAT). Lecture Notes in Computer Science, pp. 371\u2013372. Springer, New York (2011). https:\/\/doi.org\/10.1007\/978-3-642-21581-0_34","DOI":"10.1007\/978-3-642-21581-0_34"},{"issue":"1","key":"9658_CR46","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1023\/A:1006314320276","volume":"24","author":"CP Gomes","year":"2000","unstructured":"Gomes, C.P., Selman, B., Crato, N., Kautz, H.: Heavy-tailed phenomena in satisfiability and constraint satisfaction problems. Journal of Automated Reasoning 24(1), 67\u2013100 (2000). https:\/\/doi.org\/10.1023\/A:1006314320276","journal-title":"Journal of Automated Reasoning"},{"issue":"3","key":"9658_CR47","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7(3), 201\u2013215 (1960). https:\/\/doi.org\/10.1145\/321033.321034","journal-title":"Journal of the ACM"},{"issue":"7","key":"9658_CR48","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Communications of the ACM 5(7), 394\u2013397 (1962). https:\/\/doi.org\/10.1145\/368273.368557","journal-title":"Communications of the ACM"},{"key":"9658_CR49","unstructured":"Biere, A.: CaDiCaL at the SAT Race 2019. In: Proceedings of the SAT Race 2019: Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, pp. 8\u20139. University of Helsinki, Helsinki (2019)"},{"issue":"1\u20134","key":"9658_CR50","first-page":"405","volume":"64","author":"G Scollo","year":"2005","unstructured":"Scollo, G.: $$\\omega $$-rewriting the Collatz problem. Fundamenta Informaticae 64(1\u20134), 405\u2013416 (2005)","journal-title":"Fundamenta Informaticae"},{"issue":"2","key":"9658_CR51","doi-asserted-by":"publisher","first-page":"197","DOI":"10.2307\/2371809","volume":"65","author":"EL Post","year":"1943","unstructured":"Post, E.L.: Formal reductions of the general combinatorial decision problem. American Journal of Mathematics 65(2), 197\u2013215 (1943). https:\/\/doi.org\/10.2307\/2371809","journal-title":"American Journal of Mathematics"},{"issue":"1","key":"9658_CR52","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1016\/j.tcs.2007.10.020","volume":"390","author":"L De Mol","year":"2008","unstructured":"De Mol, L.: Tag systems and Collatz-like functions. Theoretical Computer Science 390(1), 92\u2013101 (2008). https:\/\/doi.org\/10.1016\/j.tcs.2007.10.020","journal-title":"Theoretical Computer Science"},{"key":"9658_CR53","doi-asserted-by":"publisher","unstructured":"Kari, J.: Cellular automata, the Collatz conjecture and powers of 3\/2. In: Proceedings of the 16th International Conference on Developments in Language Theory (DLT). Lecture Notes in Computer Science, pp. 40\u201349. Springer, New York (2012). https:\/\/doi.org\/10.1007\/978-3-642-31653-1_5","DOI":"10.1007\/978-3-642-31653-1_5"},{"issue":"1","key":"9658_CR54","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1080\/01969729508927486","volume":"26","author":"LH Kauffman","year":"1995","unstructured":"Kauffman, L.H.: Arithmetic in the form. Cybernetics and Systems 26(1), 1\u201357 (1995). https:\/\/doi.org\/10.1080\/01969729508927486","journal-title":"Cybernetics and Systems"},{"issue":"2","key":"9658_CR55","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1017\/S1446788700005371","volume":"8","author":"K Mahler","year":"1968","unstructured":"Mahler, K.: An unsolved problem on the powers of $$3\/2$$. Journal of the Australian Mathematical Society 8(2), 313\u2013321 (1968). https:\/\/doi.org\/10.1017\/S1446788700005371","journal-title":"Journal of the Australian Mathematical Society"},{"issue":"3","key":"9658_CR56","doi-asserted-by":"publisher","first-page":"877","DOI":"10.1002\/j.1538-7305.1962.tb00480.x","volume":"41","author":"T Rad\u00f3","year":"1962","unstructured":"Rad\u00f3, T.: On non-computable functions. The Bell System Technical Journal 41(3), 877\u2013884 (1962). https:\/\/doi.org\/10.1002\/j.1538-7305.1962.tb00480.x","journal-title":"The Bell System Technical Journal"},{"issue":"2","key":"9658_CR57","doi-asserted-by":"publisher","first-page":"67","DOI":"10.2307\/2689842","volume":"52","author":"P Erd\u0151s","year":"1979","unstructured":"Erd\u0151s, P.: Some unconventional problems in number theory. Mathematics Magazine 52(2), 67\u201370 (1979). https:\/\/doi.org\/10.2307\/2689842","journal-title":"Mathematics Magazine"},{"key":"9658_CR58","doi-asserted-by":"publisher","unstructured":"Waldmann, J., de Vrijer, R., Endrullis, J.: Local termination: Theory and practice. Logical Methods in Computer Science 6(3:20), (2010). https:\/\/doi.org\/10.2168\/LMCS-6(3:20)2010","DOI":"10.2168\/LMCS-6(3:20)2010"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09658-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-022-09658-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09658-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,5]],"date-time":"2023-07-05T05:11:38Z","timestamp":1688533898000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-022-09658-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,4,25]]},"references-count":58,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,6]]}},"alternative-id":["9658"],"URL":"https:\/\/doi.org\/10.1007\/s10817-022-09658-8","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,4,25]]},"assertion":[{"value":"3 December 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 December 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 April 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"15"}}