More Like this

1. The Evolution of Automated Software Repair

   https://doi.org/10.1109/TSE.2025.3533309  

   Le_Goues, Claire; Nguyen, ThanhVu; Forrest, Stephanie; Weimer, Westley (January 2025, IEEE Transactions on Software Engineering)
2. The Human Touch in Automated Fact-Checking

   Adair, Bill; Stencel, Mark; Clabby, Cathy; Li, Chengkai. (January 2019, Proceedings of the Computation + Journalism Symposium)
3. Automated Aggregator - Rewriting with the Counting Aggregate

   https://doi.org/10.4204/EPTCS.325.17  

   Dingess, Michael; Truszczynski, Miroslaw (September 2020, Electronic Proceedings in Theoretical Computer Science)

   null (Ed.)
4. An Automated Approach to the Collatz Conjecture

   https://doi.org/10.1007/978-3-030-79876-5_27  

   Yolcu, Emre; Aaronson, Scott; Heule, Marijn (July 2021, International Conference on Automated Deduction CADE-28)

   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–ternary 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. 

   more » « less
5. An Automated Approach to the Collatz Conjecture

   https://doi.org/10.1007/s10817-022-09658-8  

   Yolcu, Emre; Aaronson, Scott; Heule, Marijn J. H. (April 2023, Journal of Automated Reasoning)

   Abstract 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–ternary 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. 

   more » « less