Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
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.
Authors
- Aart Middeldorp (ORCID: https://orcid.org/0000-0001-7366-8464)
- Christina Kirk (ORCID: https://orcid.org/0000-0002-8470-2485)
Institutions
- Universität Innsbruck (AT)
Publication Details
- Published
- 2025-01-10
- DOI
- https://doi.org/10.1145/3703595.3705881
- Citations
- 1
- Primary Topic
- Logic, programming, and type systems
- Type
- article
- Field-Weighted Citation Impact
- 2.48
Funders
- Austrian Science Fund
- Universität Innsbruck