Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems

This conference talk presents a formalization of a sufficient condition for confluence of first-order left-linear rewrite systems within the Isabelle/HOL proof assistant. Explore how researchers Christina Kirk and Aart Middeldorp from the University of Innsbruck, Austria tackle Okui's 1998 criterion based on simultaneous critical pairs, which finitely represent peaks consisting of a multi-step and a normal step. Learn how this approach properly subsumes the formalized result on development-closed critical pairs. The presentation was delivered at the CPP 2025 conference (January 20-21, 2025), sponsored by ACM SIGPLAN and ACM SIGLOG. Access the full article and supplementary materials through the provided links to deepen your understanding of term rewriting, confluence, and formalization techniques.