### Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems

Julian Nagele and Aart MiddeldorpProceedings of the 7th International Conference on Interactive Theorem Proving (ITP 2016), Lecture Notes in Computer Science 9807, pp. 290 – 306, 2016.

### Abstract

This paper presents the first formalization of three classic confluence criteria for first-order term rewrite systems by Huet and Toyama. We have formalized proofs, showing that (1) linear strongly closed systems, (2) left-linear parallel closed systems, and (3) left-linear almost parallel closed systems are confluent. The third result is extended to commutation. The proofs were carried out in the proof assistant Isabelle/HOL as part of the library IsaFoR and integrated into the certifier CeTA, significantly increasing the number of certifiable proofs produced by automatic confluence tools.

### BibTeX

@inproceedings{JNAM-ITP16, author = "Julian Nagele and Aart Middeldorp", title = "Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems", booktitle = "Proceedings of the 7th International Conference on Interactive Theorem Proving", editor = "Jasmin Christian Blanchette and Stephan Merz", series = "Lecture Notes in Computer Science", volume = 9807, pages = "290--306", year = 2016, doi = "10.1007/978-3-319-43144-4_18" }