A Formalization of the Development Closedness Criterion for Left-Linear Term Rewr...

on YouTube ↗23m

" summary

Formalizes van Oostrom’s development closedness criterion for left-linear term rewrite systems by encoding multi-steps as proof terms and proving the diamond property via induction on a counted overlap measure; introduces and proves properties for residual, deletion and join operations (some newly proved), handles exhaustive position cases, and keeps to first‑order (not higher‑order). Mechanized in Isabelle/HOL (≈10,000 lines) and integrated into the certifier CeTA so tools can emit machine‑checkable confluence certificates.

AI-written summary · about

" chapters (11)

1. 0:00Introduction
2. 1:48Term rewrite systems
3. 3:14Confluence in term rewrite systems
4. 4:17Critical pairs and peaks
5. 6:25Development closeness
6. 7:50Proof terms for rewriting
7. 10:39Example application
8. 11:23Proof of closeness theorem
9. 18:51Certifying confluence with Sita
10. 19:53Conclusion
11. 20:39Q&A