{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,15]],"date-time":"2025-05-15T09:07:17Z","timestamp":1747300037858,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030798758"},{"type":"electronic","value":"9783030798765"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,5]],"date-time":"2021-07-05T00:00:00Z","timestamp":1625443200000},"content-version":"vor","delay-in-days":185,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"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. Termination of this rewriting system is equivalent to the Collatz conjecture. To show the feasibility of our approach in proving mathematically interesting statements, we implement a minimal termination prover that uses the automated method of matrix\/arctic interpretations and we perform experiments where we obtain proofs of nontrivial weakenings of the Collatz conjecture. Finally, we adapt our rewriting system to show that other open problems in mathematics can also be approached as termination problems for relatively small rewriting systems. 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\/978-3-030-79876-5_27","type":"book-chapter","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:19Z","timestamp":1625649619000},"page":"468-484","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["An Automated Approach to the Collatz Conjecture"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4255-9748","authenticated-orcid":false,"given":"Emre","family":"Yolcu","sequence":"first","affiliation":[]},{"given":"Scott","family":"Aaronson","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5587-8801","authenticated-orcid":false,"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,5]]},"reference":[{"issue":"1","key":"27_CR1","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)","journal-title":"Theoretical Computer Science"},{"key":"27_CR2","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)","DOI":"10.1017\/CBO9781139172752"},{"issue":"1","key":"27_CR3","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)","journal-title":"Acta Arithmetica"},{"issue":"1","key":"27_CR4","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)","journal-title":"Theoretical Computer Science"},{"key":"27_CR5","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) Theory and Applications of Satisfiability Testing (SAT), Lecture Notes in Computer Science, vol. 2919, pp. 502\u2013518. Springer (2004)","DOI":"10.1007\/978-3-540-24605-3_37"},{"issue":"2","key":"27_CR6","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)","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"27_CR7","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1080\/0025570X.1979.11976756","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)","journal-title":"Mathematics Magazine"},{"key":"27_CR8","doi-asserted-by":"crossref","unstructured":"Farkas, H.M.: Variants of the $$3N+1$$ conjecture and multiplicative semigroups. In: Geometry, Spectral Theory, Groups, and Dynamics, Contemporary Mathematics, vol. 387, pp. 121\u2013127. American Mathematical Society (2005)","DOI":"10.1090\/conm\/387\/07238"},{"issue":"3","key":"27_CR9","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)","journal-title":"Journal of Automated Reasoning"},{"key":"27_CR10","doi-asserted-by":"crossref","unstructured":"Hofbauer, D., Waldmann, J.: Termination of string rewriting with matrix interpretations. In: Pfenning, F. (ed.) Term Rewriting and Applications (RTA), Lecture Notes in Computer Science, vol. 4098, pp. 328\u2013342. Springer (2006)","DOI":"10.1007\/11805618_25"},{"key":"27_CR11","doi-asserted-by":"crossref","unstructured":"Kari, J.: Cellular automata, the Collatz conjecture and powers of 3\/2. In: Yen, H., Ibarra, O.H. (eds.) Developments in Language Theory (DLT), Lecture Notes in Computer Science, vol. 7410, pp. 40\u201349. Springer (2012)","DOI":"10.1007\/978-3-642-31653-1_5"},{"key":"27_CR12","doi-asserted-by":"crossref","unstructured":"Ka\u0161\u010d\u00e1k, F.: Small universal one-state linear operator algorithm. In: Havel, I.M., Koubek, V. (eds.) Mathematical Foundations of Computer Science (MFCS), Lecture Notes in Computer Science, vol. 629, pp. 327\u2013335. Springer (1992)","DOI":"10.1007\/3-540-55808-X_31"},{"issue":"1","key":"27_CR13","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)","journal-title":"Cybernetics and Systems"},{"issue":"3","key":"27_CR14","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)","journal-title":"Advances in Applied Mathematics"},{"issue":"2","key":"27_CR15","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"},{"issue":"1","key":"27_CR16","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1080\/00029890.1985.11971528","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)","journal-title":"The American Mathematical Monthly"},{"key":"27_CR17","doi-asserted-by":"crossref","unstructured":"Lagarias, J.C.: The Ultimate Challenge: The $$3x+1$$ Problem. American Mathematical Society (2010)","DOI":"10.1090\/mbk\/078"},{"key":"27_CR18","unstructured":"Lagarias, J.C.: The $$3x+1$$ problem: An annotated bibliography (1963\u20131999) (2011), arXiv:math\/0309224"},{"key":"27_CR19","unstructured":"Lagarias, J.C.: The $$3x+1$$ problem: An annotated bibliography, II (2000\u20132009) (2012), arXiv:math\/0608208"},{"issue":"2","key":"27_CR20","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)","journal-title":"Journal of the Australian Mathematical Society"},{"key":"27_CR21","doi-asserted-by":"crossref","unstructured":"Michel, P.: Problems in number theory from busy beaver competition. Logical Methods in Computer Science 11(4:10), 1\u201335 (2015)","DOI":"10.2168\/LMCS-11(4:10)2015"},{"key":"27_CR22","doi-asserted-by":"crossref","unstructured":"Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisfiability solvers. In: Marques-Silva, J., Sakallah, K.A. (eds.) Theory and Applications of Satisfiability Testing (SAT), Lecture Notes in Computer Science, vol. 4501, pp. 294\u2013299. Springer (2007)","DOI":"10.1007\/978-3-540-72788-0_28"},{"issue":"2","key":"27_CR23","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)","journal-title":"American Journal of Mathematics"},{"issue":"3","key":"27_CR24","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1080\/0025570X.1985.11977179","volume":"58","author":"DA Rawsthorne","year":"1985","unstructured":"Rawsthorne, D.A.: Imitation of an iteration. Mathematics Magazine 58(3), 172\u2013176 (1985)","journal-title":"Mathematics Magazine"},{"issue":"1\u20134","key":"27_CR25","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"},{"key":"27_CR26","doi-asserted-by":"crossref","unstructured":"Sternagel, C., Thiemann, R.: Formalizing monotone algebras for certification of termination and complexity proofs. In: Dowek, G. (ed.) Rewriting and Typed Lambda Calculi (RTA-TLCA), Lecture Notes in Computer Science, vol. 8560, pp. 441\u2013455. Springer (2014)","DOI":"10.1007\/978-3-319-08918-8_30"},{"issue":"1","key":"27_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)","journal-title":"The Mathematical Intelligencer"},{"key":"27_CR28","doi-asserted-by":"crossref","unstructured":"Waldmann, J., de Vrijer, R., Endrullis, J.: Local termination: Theory and practice. Logical Methods in Computer Science 6(3) (2010)","DOI":"10.2168\/LMCS-6(3:20)2010"},{"issue":"2","key":"27_CR29","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)","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 28"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-79876-5_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:33:06Z","timestamp":1625650386000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-79876-5_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030798758","9783030798765"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-79876-5_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"5 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.cmu.edu\/~mheule\/CADE28\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"76","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"38% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2 invited papers and 7 system descriptions are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}