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
}