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 Entry

@inproceedings{NM-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"
}