Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs

Explore a 31-minute conference talk from CPP 2024 that delves into the formalization of parallel critical pairs (PCPs) and their application in certifying confluence and commutation proofs for term rewrite systems. Learn how researchers simplified the definition of PCPs using a context-based approach, leading to a more efficient recursive algorithm for PCP computation. Discover how this work extends existing criteria from confluence to commutation and its integration into the CeTA certifier, enabling validation of proofs generated by the Hakusan automatic confluence tool. Gain insights into the impact of this research on certifying previously uncertified confluence proofs for certain term rewrite systems.