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