{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T00:59:17Z","timestamp":1767920357569,"version":"3.49.0"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>Equations are ubiquitous in mathematical reasoning.  \nOften, however, they only hold under certain conditions.  \nAs these conditions are usually clear from context, mathematicians regularly omit them when performing equational reasoning on paper.  \nIn contrast, interactive theorem provers pedantically insist on every detail to be convinced that a theorem holds, hindering equational reasoning at the more abstract level of pen-and-paper mathematics.  \nIn this paper, we address this issue by raising the level of equational reasoning to enable pen-and-paper style in interactive theorem provers.  \nWe achieve this by interpreting theorems as conditional rewrite rules, and use equality saturation to automatically derive equational proofs.  \nConditions that cannot be automatically proven may be surfaced as proof obligations.  \nConcretely, we present how to interpret theorems as conditional rewrite rules for a significant class of theorems.  \nHandling these theorems goes beyond simple syntactic rewriting, and deals with aspects like propositional conditions and type classes.  \nWe evaluate our approach by implementing it as a tactic in Lean, using the egg library for equality saturation with e-graphs.  \nWe show four use cases demonstrating the efficacy of this higher level of abstraction for equational reasoning.<\/jats:p>","DOI":"10.1145\/3776667","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"718-747","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-3567-6890","authenticated-orcid":false,"given":"Marcus","family":"Rossel","sequence":"first","affiliation":[{"name":"Barkhausen Institut, Dresden, Germany"},{"name":"Technische Universit\u00e4t Darmstadt, Darmstadt, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-9151-773X","authenticated-orcid":false,"given":"Rudi","family":"Schneider","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t Berlin, Berlin, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8461-8075","authenticated-orcid":false,"given":"Thomas","family":"K\u0153hler","sequence":"additional","affiliation":[{"name":"ICube Lab - CNRS - Universit\u00e9 de Strasbourg, Strasbourg, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5048-0741","authenticated-orcid":false,"given":"Michel","family":"Steuwer","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t Berlin, Berlin, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0409-1363","authenticated-orcid":false,"given":"Andr\u00e9s","family":"Goens","sequence":"additional","affiliation":[{"name":"University of Amsterdam, Amsterdam, Netherlands"},{"name":"Technische Universit\u00e4t Darmstadt, Darmstadt, Germany"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020","author":"Blanchette Jasmin","year":"2020","unstructured":"Jasmin Blanchette and Catalin Hritcu (Eds.). 2020. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020. ACM, 367\u2013381. https:\/\/doi.org\/10.1145\/3372885.3373824 10.1145\/3372885.3373824"},{"key":"e_1_2_1_2_1","volume-title":"Optimizing Beta Reduction in E-Graphs. https:\/\/pldi23.sigplan.org\/details\/egraphs-2023-papers\/12\/Optimizing-Beta-Reduction-in-E-Graphs EGRAPHS 2023","author":"Gonzalez Emmanuel Anaya","unstructured":"Emmanuel Anaya Gonzalez, Cole Kurashige, Aditya Giridharan, and Polikarpova Nadia. 2023. Optimizing Beta Reduction in E-Graphs. https:\/\/pldi23.sigplan.org\/details\/egraphs-2023-papers\/12\/Optimizing-Beta-Reduction-in-E-Graphs EGRAPHS 2023"},{"key":"e_1_2_1_3_1","volume-title":"CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, Ganesh Gopalakrishnan and Shaz Qadeer (Eds.) (Lecture Notes in Computer Science","volume":"177","author":"Barrett Clark W.","year":"2011","unstructured":"Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011. CVC4. In Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, Ganesh Gopalakrishnan and Shaz Qadeer (Eds.) (Lecture Notes in Computer Science, Vol. 6806). Springer, 171\u2013177. https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14 10.1007\/978-3-642-22110-1_14"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(87)80027-5"},{"key":"e_1_2_1_5_1","volume-title":"8th International Symposium, FroCoS 2011, Saarbr\u00fccken, Germany, October 5-7, 2011. Proceedings, Cesare Tinelli and Viorica Sofronie-Stokkermans (Eds.) (Lecture Notes in Computer Science","volume":"27","author":"Blanchette Jasmin Christian","year":"2011","unstructured":"Jasmin Christian Blanchette, Lukas Bulwahn, and Tobias Nipkow. 2011. Automatic Proof and Disproof in Isabelle\/HOL. In Frontiers of Combining Systems, 8th International Symposium, FroCoS 2011, Saarbr\u00fccken, Germany, October 5-7, 2011. Proceedings, Cesare Tinelli and Viorica Sofronie-Stokkermans (Eds.) (Lecture Notes in Computer Science, Vol. 6989). Springer, 12\u201327. https:\/\/doi.org\/10.1007\/978-3-642-24364-6_2 10.1007\/978-3-642-24364-6_2"},{"key":"e_1_2_1_6_1","volume-title":"Zoltan Kocsis, Bruno Le Floch, Amir Livne Bar-on, Lorenzo Luccioli, Douglas McNeil, Alex Meiburg, Pietro Monticone, Pace P. Nielsen, Giovanni Paolini, Marco Petracci","author":"Bolan Matthew","year":"2026","unstructured":"Matthew Bolan, Joachim Breitner, Jose Brox, Nicholas Carlini, Mario Carneiro, Floris van Doorn, Martin Dvorak, Andr\u00e9s Goens, Aaron Hill, Harald Husum, Hern\u00e1n Ibarra Mejia, Zoltan Kocsis, Bruno Le Floch, Amir Livne Bar-on, Lorenzo Luccioli, Douglas McNeil, Alex Meiburg, Pietro Monticone, Pace P. Nielsen, Giovanni Paolini, Marco Petracci, Bernhard Reinke, David Renshaw, Marcus Rossel, Cody Roux, J\u00e9r\u00e9my Scanvic, Shreyas Srinivas, Anand Rao Tadipatri, Terence Tao, Vlad Tsyrklevich, Fernando Vaquerizo-Villar, Daniel Weber, and Fan Zheng. 2026. The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale. In preparation"},{"key":"e_1_2_1_7_1","unstructured":"Thomas Bourgeat. 2023. Specification and verification of sequential machines in rule-based hardware languages. Ph. D. Dissertation. MIT USA. https:\/\/hdl.handle.net\/1721.1\/150194"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 3rd International Joint Conference on Artificial Intelligence","author":"Boyer Robert S.","year":"1973","unstructured":"Robert S. Boyer and J Strother Moore. 1973. Proving Theorems about LISP Functions. In Proceedings of the 3rd International Joint Conference on Artificial Intelligence. Standford, CA, USA, August 20-23, 1973, Nils J. Nilsson (Ed.). William Kaufmann, 486\u2013493. http:\/\/ijcai.org\/Proceedings\/73\/Papers\/053.pdf"},{"key":"e_1_2_1_9_1","volume-title":"The Type Theory of Lean. Master\u2019s thesis","author":"Carneiro Mario","unstructured":"Mario Carneiro. 2019. The Type Theory of Lean. Master\u2019s thesis. Carnegie Mellon University."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2403.14064"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-011-9225-2"},{"key":"e_1_2_1_12_1","volume-title":"Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules. In 25th International Conference on Types for Proofs and Programs, TYPES 2019","volume":"27","author":"Cockx Jesper","year":"2019","unstructured":"Jesper Cockx. 2019. Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules. In 25th International Conference on Types for Proofs and Programs, TYPES 2019, June 11-14, 2019, Oslo, Norway, Marc Bezem and Assia Mahboubi (Eds.) (LIPIcs, Vol. 175). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2:1\u20132:27. https:\/\/doi.org\/10.4230\/LIPICS.TYPES.2019.2 10.4230\/LIPICS.TYPES.2019.2"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_2_1_14_1","volume-title":"International Conference on Computer Logic, Tallinn, USSR","volume":"66","author":"Coquand Thierry","year":"1988","unstructured":"Thierry Coquand and Christine Paulin. 1988. Inductively defined types. In COLOG-88, International Conference on Computer Logic, Tallinn, USSR, December 1988, Proceedings, Per Martin-L\u00f6f and Grigori Mints (Eds.) (Lecture Notes in Computer Science, Vol. 417). Springer, 50\u201366. https:\/\/doi.org\/10.1007\/3-540-52335-9_47 10.1007\/3-540-52335-9_47"},{"key":"e_1_2_1_15_1","volume-title":"Workshop on Controlled Natural Language, CNL 2009","author":"Cramer Marcos","year":"2009","unstructured":"Marcos Cramer, Bernhard Fisseni, Peter Koepke, Daniel K\u00fchlwein, Bernhard Schr\u00f6der, and Jip Veldman. 2009. The Naproche Project Controlled Natural Language Proof Checking of Mathematical Texts. In Controlled Natural Language, Workshop on Controlled Natural Language, CNL 2009, Marettimo Island, Italy, June 8-10, 2009. Revised Papers, Norbert E. Fuchs (Ed.) (Lecture Notes in Computer Science, Vol. 5972). Springer, 170\u2013186. https:\/\/doi.org\/10.1007\/978-3-642-14418-9_11 10.1007\/978-3-642-14418-9_11"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-018-9458-4"},{"key":"e_1_2_1_17_1","unstructured":"NG de Bruijn. 1968. Automath: a language for mathematics."},{"key":"e_1_2_1_18_1","volume-title":"Studies in Logic and the Foundations of Mathematics. 133","author":"De Bruijn Nicolaas Govert","unstructured":"Nicolaas Govert De Bruijn. 1994. A survey of the project AUTOMATH. In Studies in Logic and the Foundations of Mathematics. 133, Elsevier, 141\u2013161."},{"key":"e_1_2_1_19_1","unstructured":"Leonardo de Moura and Kim Morrison. 2025. The Lean Language Reference: The grind tactic. https:\/\/lean-lang.org\/doc\/reference\/latest\/The\u2013grind\u2013tactic\/##grind"},{"key":"e_1_2_1_20_1","volume-title":"Virtual Event","volume":"635","author":"de Moura Leonardo","year":"2021","unstructured":"Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 Theorem Prover and Programming Language. In Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, Andr\u00e9 Platzer and Geoff Sutcliffe (Eds.) (Lecture Notes in Computer Science, Vol. 12699). Springer, 625\u2013635. https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37 10.1007\/978-3-030-79876-5_37"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_2_1_23_1","volume-title":"CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, Rupak Majumdar and Viktor Kuncak (Eds.) (Lecture Notes in Computer Science","volume":"133","author":"Ekici Burak","unstructured":"Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, and Clark W. Barrett. 2017. SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. In Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, Rupak Majumdar and Viktor Kuncak (Eds.) (Lecture Notes in Computer Science, Vol. 10427). Springer, 126\u2013133. https:\/\/doi.org\/10.1007\/978-3-319-63390-9_7 10.1007\/978-3-319-63390-9_7"},{"key":"e_1_2_1_24_1","volume-title":"Introduction to Lie algebras. 122","author":"Erdmann Karin","unstructured":"Karin Erdmann and Mark J Wildon. 2006. Introduction to Lie algebras. 122, Springer."},{"key":"e_1_2_1_25_1","volume-title":"FMCAD 2022","author":"Flatt Oliver","year":"2022","unstructured":"Oliver Flatt, Samuel Coward, Max Willsey, Zachary Tatlock, and Pavel Panchekha. 2022. Small Proofs from Congruence Closure. In 22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, October 17-21, 2022, Alberto Griggio and Neha Rungta (Eds.). IEEE, 75\u201383. https:\/\/doi.org\/10.34727\/2022\/ISBN.978-3-85448-053-2_13 10.34727\/2022\/ISBN.978-3-85448-053-2_13"},{"key":"e_1_2_1_26_1","volume-title":"18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, Joe Hurd and Thomas F. Melham (Eds.) (Lecture Notes in Computer Science","volume":"113","author":"Gr\u00e9goire Benjamin","year":"2005","unstructured":"Benjamin Gr\u00e9goire and Assia Mahboubi. 2005. Proving Equalities in a Commutative Ring Done Right in Coq. In Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, Joe Hurd and Thomas F. Melham (Eds.) (Lecture Notes in Computer Science, Vol. 3603). Springer, 98\u2013113. https:\/\/doi.org\/10.1007\/11541868_7 10.1007\/11541868_7"},{"key":"e_1_2_1_27_1","volume-title":"Proc. ACM Program. Lang., 4, ICFP","author":"Hagedorn Bastian","year":"2020","unstructured":"Bastian Hagedorn, Johannes Lenfers, Thomas Koehler, Xueying Qin, Sergei Gorlatch, and Michel Steuwer. 2020. Achieving high-performance the functional way: a functional pearl on expressing high-performance optimizations as rewrite strategies. Proc. ACM Program. Lang., 4, ICFP (2020), 92:1\u201392:29. https:\/\/doi.org\/10.1145\/3408974 10.1145\/3408974"},{"key":"e_1_2_1_28_1","unstructured":"Muhammad Humayoun. 2010. Mathnat-mathematical text in a controlled natural language. Special issue: Natural Language Processing and its\u2026."},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the Tenth Symposium on Trends in Functional Programming, TFP 2009","author":"Daniel W.","year":"2009","unstructured":"Daniel W. H. James and Ralf Hinze. 2009. A Reflection-based Proof Tactic for Lattices in Coq. In Proceedings of the Tenth Symposium on Trends in Functional Programming, TFP 2009, Kom\u00e1rno, Slovakia, June 2-4, 2009, Zolt\u00e1n Horv\u00e1th, Vikt\u00f3ria Zs\u00f3k, Peter Achten, and Pieter W. M. Koopman (Eds.) (Trends in Functional Programming, Vol. 10). Intellect, 97\u2013112."},{"key":"e_1_2_1_30_1","volume-title":"The Eleventh International Conference on Learning Representations , ICLR 2023","author":"Jiang Albert Qiaochu","year":"2023","unstructured":"Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timoth \u00e9e Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. 2023. Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs. In The Eleventh International Conference on Learning Representations , ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net. https:\/\/openreview.net\/forum?id=SMa9EAovKMC"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5525\/GLA.THESIS.83323"},{"key":"e_1_2_1_32_1","volume-title":"Proc. ACM Program. Lang., 8, POPL","author":"Koehler Thomas","year":"2024","unstructured":"Thomas Koehler, Andr\u00e9s Goens, Siddharth Bhat, Tobias Grosser, Phil Trinder, and Michel Steuwer. 2024. Guided Equality Saturation. Proc. ACM Program. Lang., 8, POPL (2024), 1727\u20131758. https:\/\/doi.org\/10.1145\/3632900 10.1145\/3632900"},{"key":"e_1_2_1_33_1","volume-title":"Techniques for Program Verification","author":"Nelson Charles Gregory","unstructured":"Charles Gregory Nelson. 1980. Techniques for Program Verification. Stanford University."},{"key":"e_1_2_1_34_1","volume-title":"16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings, J\u00fcrgen Giesl (Ed.) (Lecture Notes in Computer Science","volume":"468","author":"Nieuwenhuis Robert","year":"2005","unstructured":"Robert Nieuwenhuis and Albert Oliveras. 2005. Proof-Producing Congruence Closure. In Term Rewriting and Applications, 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings, J\u00fcrgen Giesl (Ed.) (Lecture Notes in Computer Science, Vol. 3467). Springer, 453\u2013468. https:\/\/doi.org\/10.1007\/978-3-540-32033-3_33 10.1007\/978-3-540-32033-3_33"},{"key":"e_1_2_1_35_1","volume-title":"Isabelle: The Next 700 Theorem Provers. CoRR, cs.LO\/9301106","author":"Paulson Lawrence C.","year":"1993","unstructured":"Lawrence C. Paulson. 1993. Isabelle: The Next 700 Theorem Provers. CoRR, cs.LO\/9301106 (1993), arxiv:cs\/9301106"},{"key":"e_1_2_1_36_1","first-page":"2","article-title":"The design and implementation of VAMPIRE","volume":"15","author":"Riazanov Alexandre","year":"2002","unstructured":"Alexandre Riazanov and Andrei Voronkov. 2002. The design and implementation of VAMPIRE. AI Commun., 15, 2-3 (2002), 91\u2013110. http:\/\/content.iospress.com\/articles\/ai-communications\/aic259","journal-title":"AI Commun."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","unstructured":"Rocq Dev Team. 2025. The Rocq Prover. https:\/\/doi.org\/10.5281\/zenodo.15149629 10.5281\/zenodo.15149629","DOI":"10.5281\/zenodo.15149629"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.17696648"},{"key":"e_1_2_1_39_1","unstructured":"Joseph J Rotman. 2006. A first course in abstract algebra: with applications. Pearson."},{"key":"e_1_2_1_40_1","volume-title":"Proc. ACM Program. Lang., 9, PLDI (2025)","author":"Schneider Rudi","year":"2025","unstructured":"Rudi Schneider, Marcus Rossel, Amir Shaikhha, Andr\u00e9s Goens, Thomas Koehler, and Michel Steuwer. 2025. Slotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs. Proc. ACM Program. Lang., 9, PLDI (2025), 1888\u20131910. https:\/\/doi.org\/10.1145\/3729326 10.1145\/3729326"},{"key":"e_1_2_1_41_1","volume-title":"IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings, Nicola Olivetti and Ashish Tiwari (Eds.) (Lecture Notes in Computer Science","volume":"115","author":"Selsam Daniel","year":"2016","unstructured":"Daniel Selsam and Leonardo de Moura. 2016. Congruence Closure in Intensional Type Theory. In Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings, Nicola Olivetti and Ashish Tiwari (Eds.) (Lecture Notes in Computer Science, Vol. 9706). Springer, 99\u2013115. https:\/\/doi.org\/10.1007\/978-3-319-40229-1_8 10.1007\/978-3-319-40229-1_8"},{"key":"e_1_2_1_42_1","volume-title":"FMCAD 2024","author":"Singher Eytan","year":"2024","unstructured":"Eytan Singher and Shachar Itzhaky. 2024. Easter Egg: Equality Reasoning Based on E-Graphs with Multiple Assumptions. In Formal Methods in Computer-Aided Design, FMCAD 2024, Prague, Czech Republic, October 15-18, 2024, Nina Narodytska and Philipp R\u00fcmmer (Eds.). IEEE, 70\u201383. https:\/\/doi.org\/10.34727\/2024\/ISBN.978-3-85448-065-5_13 10.34727\/2024\/ISBN.978-3-85448-065-5_13"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3706056"},{"key":"e_1_2_1_44_1","doi-asserted-by":"crossref","first-page":"703","DOI":"10.2307\/2371008","article-title":"Postulates for Boolean algebras and generalized Boolean algebras","volume":"57","author":"Stone Marshall H","year":"1935","unstructured":"Marshall H Stone. 1935. Postulates for Boolean algebras and generalized Boolean algebras. American Journal of Mathematics, 57, 4 (1935), 703\u2013732.","journal-title":"American Journal of Mathematics"},{"key":"e_1_2_1_45_1","volume-title":"Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009","author":"Tate Ross","year":"2009","unstructured":"Ross Tate, Michael Stepp, Zachary Tatlock, and Sorin Lerner. 2009. Equality saturation: a new approach to optimization. In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009, Zhong Shao and Benjamin C. Pierce (Eds.). ACM, 264\u2013276. https:\/\/doi.org\/10.1145\/1480881.1480915 10.1145\/1480881.1480915"},{"key":"e_1_2_1_46_1","volume-title":"Proceedings of the 9th International Joint Conference on Artificial Intelligence","author":"Trybulec Andrzej","year":"1985","unstructured":"Andrzej Trybulec and Howard A. Blair. 1985. Computer Assisted Reasoning with MIZAR. In Proceedings of the 9th International Joint Conference on Artificial Intelligence. Los Angeles, CA, USA, August 1985, Aravind K. Joshi (Ed.). Morgan Kaufmann, 26\u201328. http:\/\/ijcai.org\/Proceedings\/85-1\/Papers\/006.pdf"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.5445\/IR\/1000161074"},{"key":"e_1_2_1_48_1","volume-title":"Isar - a versatile environment for human readable formal proof documents. Ph. D. Dissertation","author":"Wenzel Markus","year":"2002","unstructured":"Markus Wenzel. 2002. Isabelle, Isar - a versatile environment for human readable formal proof documents. Ph. D. Dissertation. Technical University Munich, Germany. http:\/\/tumb1.biblio.tu-muenchen.de\/publ\/diss\/in\/2002\/wenzel.pdf"},{"key":"e_1_2_1_49_1","volume-title":"Scott (Lecture Notes in Computer Science","volume":"4","author":"Ed Freek Wiedijk","year":"2006","unstructured":"Freek Wiedijk (Ed.). 2006. The Seventeen Provers of the World, Foreword by Dana S. Scott (Lecture Notes in Computer Science, Vol. 3600). Springer. isbn:3-540-30704-4 https:\/\/doi.org\/10.1007\/11542384 10.1007\/11542384"},{"key":"e_1_2_1_50_1","volume-title":"CICM 2023, Cambridge, UK, September 5-8, 2023, Proceedings, Catherine Dubois and Manfred Kerber (Eds.) (Lecture Notes in Computer Science","volume":"236","author":"Wieser Eric","year":"2023","unstructured":"Eric Wieser. 2023. Multiple-Inheritance Hazards in Dependently-Typed Algebraic Hierarchies. In Intelligent Computer Mathematics - 16th International Conference, CICM 2023, Cambridge, UK, September 5-8, 2023, Proceedings, Catherine Dubois and Manfred Kerber (Eds.) (Lecture Notes in Computer Science, Vol. 14101). Springer, 222\u2013236. https:\/\/doi.org\/10.1007\/978-3-031-42753-4_15 10.1007\/978-3-031-42753-4_15"},{"key":"e_1_2_1_51_1","volume-title":"Proc. ACM Program. Lang., 5, POPL","author":"Willsey Max","year":"2021","unstructured":"Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. 2021. egg: Fast and extensible equality saturation. Proc. ACM Program. Lang., 5, POPL (2021), 1\u201329. https:\/\/doi.org\/10.1145\/3434304 10.1145\/3434304"},{"key":"e_1_2_1_52_1","volume-title":"Dis\/Equality Graphs. Proc. ACM Program. Lang., 9, POPL","author":"Zakhour George","year":"2025","unstructured":"George Zakhour, Pascal Weisenburger, Jahrim Gabriele Cesario, and Guido Salvaneschi. 2025. Dis\/Equality Graphs. Proc. ACM Program. Lang., 9, POPL (2025), 2282\u20132305. https:\/\/doi.org\/10.1145\/3704913 10.1145\/3704913"},{"key":"e_1_2_1_53_1","volume-title":"Proc. ACM Program. Lang., 7, PLDI","author":"Zhang Yihong","year":"2023","unstructured":"Yihong Zhang, Yisu Remy Wang, Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, and Max Willsey. 2023. Better Together: Unifying Datalog and Equality Saturation. Proc. ACM Program. Lang., 7, PLDI (2023), 468\u2013492. https:\/\/doi.org\/10.1145\/3591239 10.1145\/3591239"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2504.14340"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776667","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T19:05:55Z","timestamp":1767899155000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776667"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":54,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776667"],"URL":"https:\/\/doi.org\/10.1145\/3776667","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}