Publications in 2025
Automated Strategy Invention for Confluence of Term Rewrite Systems
Liao Zhang, Fabian Mitterwallner, Jan Jakubův, Cezary Kaliszyk
International Joint Conference on Artificial Intelligence,
pp. 4724-4732,
2025.
Path Equivalence and Automation for Integration Contours
Manuel Eberl
Archive of Formal Proofs 2025.
An Isabelle/HOL Formalization of Semi-Thue and Conditional Semi-Thue Systems
Dohan Kim
International Conference on Interactive Theorem Proving,
Leibniz International Proceedings in Informatics 352,
pp. 10:1—10:20,
2025.
Verifying an Efficient Algorithm for Computing Bernoulli Numbers
Manuel Eberl, Peter Lammich
International Conference on Interactive Theorem Proving (ITP),
2025.
The Dependently Typed Higher-Order Form for the TPTP World
Daniel Ranalter, Cezary Kaliszyk, Florian Rabe, Geoff Sutcliffe
15th International Symposium on Frontiers of Combining Systems,
Lecture Notes in Artificial Intelligence 15979,
pp. 287-305,
2025.
Characterizing Equivalence of Logically Constrained Terms via Existentially Constrained Terms
Kanta Takahata, Jonas Schöpf, Naoki Nishida, Takahito Aoto
Logic-Based Program Synthesis and Transformation,
Lecture Notes in Computer Science 16117,
pp. 180-195,
2025.
The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting
Johannes Niederhauser, Aart Middeldorp
30th International Conference on Automated Deduction,
Lecture Notes in Artificial Intelligence 15943,
pp. 207-225,
2025.
Hydra Battles and AC Termination
Nao Hirokawa and Aart Middeldorp
Logical Methods in Computer Science 21(2),
pp. 29:1-29:22,
2025.
Left-Linear Completion with AC Axioms
Johannes Niederhauser, Nao Hirokawa, Aart Middeldorp
Logical Methods in Computer Science,
21(2),
pp. 10:1-10:44,
2025.
Automated Analysis of Logically Constrained Rewrite Systems using crest
Jonas Schöpf, Aart Middeldorp
Proceedings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2025),
Lecture Notes in Computer Science 15696,
pp. 124-144,
2025.
First-Order Rewriting
René Thiemann, Christian Sternagel, Christina Kirk, Martin Avanzini, Bertram Felgenhauer, Julian Nagele, Thomas Sternagel, Sarah Winkler, Akihisa Yamada
Archive of Formal Proofs 2025.
Congruence Closure Modulo Groups
Dohan Kim
Logical Methods in Computer Science 2025.
An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting
Dohan Kim, Teppei Saito, René Thiemann, and Akihisa Yamada
Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2025),
2025.
Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
Christina Kirk, Aart Middeldorp
Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2025),
pp. 156-170,
2025.