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.
Abstract
In this paper, we present an Isabelle/HOL formalization of corewrite pairs for non-reachability analysis in term rewriting. In particular, we formalize polynomial interpretations over negative integers as well as the weighted path order (WPO) and its variant co-WPO. With this formalization, the verified certifier CeTA is now able to check such non-reachability proofs, including those for non-reachability problems of a database where existing tools fail to provide certified proofs.
BibTex
@inproceedings{DBLP:conf/cpp/0001ST025,author = {Dohan Kim and Teppei Saito and Ren{\’{e}} Thiemann and Akihisa Yamada},editor = {Kathrin Stark and Amin Timany and Sandrine Blazy and Nicolas Tabareau},title = {An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting},booktitle = {Proceedings of the 14th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, {CPP} 2025, Denver, CO, USA, January 20-21, 2025},pages = {272—282},publisher = {{ACM}}, year = {2025}, url = {https://doi.org/10.1145/3703595.3705889}, doi = {10.1145/3703595.3705889}, timestamp = {Mon, 03 Mar 2025 21:01:02 +0100}, biburl = {https://dblp.org/rec/conf/cpp/0001ST025.bib}, bibsource = {dblp computer science bibliography, https://dblp.org}}
- Details
- Category: Publications 2025
Johannes Niederhauser, Nao Hirokawa, Aart Middeldorp
Logical Methods in Computer Science, 21(2), pp. 10:1-10:44, 2025.
pdf 
doi:10.46298/LMCS-21(2:10)2025
Abstract
We revisit completion modulo equational theories for left-linear term rewrite systems where unification modulo the theory is avoided and the normal rewrite relation can be used in order to decide validity questions. To that end, we give a new correctness proof for finite runs and establish a simulation result between the two inference systems known from the literature. Given a concrete reduction order, novel canonicity results show that the resulting complete systems are unique up to the representation of their rules’ right-hand sides. Furthermore, we show how left-linear AC completion can be simulated by general AC completion. In particular, this result allows us to switch from the former to the latter at any point during a completion process.
BibTex
@article{NHM-LMCS21, author = "Johannes Niederhauser and Nao Hirokawa and Aart Middeldorp", title = "Left-Linear Completion with {AC} Axioms", journal = "Logical Methods in Computer Science", volume = 21, number = 2, pages = "10:1--10:44", year = 2025, doi = "10.46298/LMCS-21(2:10)2025"}
- Details
- Category: Publications 2025
Dohan Kim
Logical Methods in Computer Science 2025.
Abstract
his paper presents a new framework for constructing congruence closure of a finite set of ground equations over uninterpreted symbols and interpreted symbols for the group axioms. In this framework, ground equations are flattened into certain forms by introducing new constants, and a completion procedure is performed on ground flat equations. The proposed completion procedure uses equational inference rules and constructs a ground convergent rewrite system for congruence closure with such interpreted symbols. If the completion procedure terminates, then it yields a decision procedure for the word problem for a finite set of ground equations with respect to the group axioms. This paper also provides a sufficient terminating condition of the completion procedure for constructing a ground convergent rewrite system from ground flat equations containing interpreted symbols for the group axioms. In addition, this paper presents a new method for constructing congruence closure of a finite set of ground equations containing interpreted symbols for the semigroup, monoid, and the multiple disjoint sets of group axioms, respectively, using the proposed framework.
BibTex
@article{DBLP:journals/lmcs/Kim25, author = {Dohan Kim}, title = {Congruence Closure Modulo Groups}, journal = {Log. Methods Comput. Sci.}, volume = {21}, number = {1}, year = {2025}, url = {https://doi.org/10.46298/lmcs-21(1:20)2025}, doi = {10.46298/LMCS-21(1:20)2025}, timestamp = {Fri, 04 Apr 2025 16:39:05 +0200}, biburl = {https://dblp.org/rec/journals/lmcs/Kim25.bib}, bibsource = {dblp computer science bibliography, https://dblp.org}}
- Details
- Category: Publications 2025
René Thiemann, Christian Sternagel, Christina Kirk, Martin Avanzini, Bertram Felgenhauer, Julian Nagele, Thomas Sternagel, Sarah Winkler, Akihisa Yamada
Archive of Formal Proofs 2025.
Abstract
This entry, derived from the Isabelle Formalization of Rewriting (IsaFoR), provides a formalized foundation for first-order term rewriting. This serves as the basis for the certifier CeTA, which is generated from IsaFoR and verifies termination, confluence, and complexity proofs for term rewrite systems (TRSs). This formalization covers fundamental results for term rewriting, as presented in the foundational textbooks by Baader and Nipkow and TeReSe. These include:
- Various types of rewrite steps, such as root, ground, parallel, and multi-steps.
- Special cases of TRSs, such as linear and left-linear TRSs.
- A definition of critical pairs and key results, including the critical pair lemma.
- Orthogonality, notably that weak orthogonality implies confluence.
- Executable versions of relevant definitions, such as parallel and multi-step rewriting.
BibTex
@article{First_Order_Rewriting-AFP, author = {René Thiemann and Christian Sternagel and Christina Kirk and Martin Avanzini and Bertram Felgenhauer and Julian Nagele and Thomas Sternagel and Sarah Winkler and Akihisa Yamada}, title = {First-Order Rewriting}, journal = {Archive of Formal Proofs}, month = {April}, year = {2025}, note = {\url{https://isa-afp.org/entries/First_Order_Rewriting.html}, Formal proof development}, ISSN = {2150-914x},}
- Details
- Category: Publications 2025
Christina Kirk, Aart Middeldorp
Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2025), pp. 156-170, 2025.
pdf doi:10.1145/3703595.3705881
Abstract
We report on the formalization of a sufficient condition for confluence of first-order left-linear rewrite systems within the proof assistant Isabelle/HOL. This criterion, originally proposed by Okui (1998), is based on simultaneous critical pairs, which finitely represent peaks consisting of a multi-step and a normal step. It properly subsumes the formalized result on development-closed critical pairs.
BibTex
@inproceedings{CKAM-CPP25, author = "Christina Kirk and Aart Middeldorp", title = "Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems", booktitle = "Proceedings of the 14th International {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs", editors = "Kathrin Stark and Amin Timany and Sandrine Blazy and Nicolas Tabareau", publisher = "ACM", pages = "156--170", doi = "10.1145/3703595.3705881", year = 2025}
- Details
- Category: Publications 2025
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.
pdf doi:10.46298/LMCS-21(2:10)2025doi:10.46298/LMCS-21(2:10)2025
Abstract
We present crest, a tool for automatically proving (non-)confluence and termination of logically constrained rewrite systems. We compare crest to other tools for logically constrained rewriting. Extensive experiments demonstrate the promise of crest.
BibTex
@inproceedings{SM-TACAS25, author = "Jonas Schöpf and Aart Middeldorp", title = "Automated Analysis of Logically Constrained Rewrite Systems using crest", booktitle = "Proceedings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems", editor = "Arie Gurfunkel and Marijn Heule", series = "Lecture Notes in Computer Science", volume = 15696, pages = "124--144", year = 2025, doi = "10.1007/978-3-031-90643-5_7"}
- Details
- Category: Publications 2025