cl-banner

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

Julian Nagele and Aart Middeldorp

Proceedings 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.

 

  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"
}
Nach oben scrollen