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

Julian Nagele and Aart Middeldorp

Proceedings of the 7^th 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.

  PDF |    doi:10.1007/978-3-319-43144-4_18

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"
}