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 Entry

@inproceedings{KM-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",
 pages     = "156--170",
 doi       = "10.1145/3703595.3705881",
 year      = 2025
}