cl-banner

A New and Formalized Proof of Abstract Completion

Nao Hirokawa, Aart Middeldorp, and Christian Sternagel

Proceedings of the 5th International Conference on Interactive Theorem Proving (ITP 2014), Lecture Notes in Computer Science 8558, pp. 292 – 307, 2014.

Abstract

Completion is one of the most studied techniques in term rewriting. We present a new proof of the correctness of abstract completion that is based on peak decreasingness, a special case of decreasing diagrams. Peak decreasingness replaces Newman’s Lemma and allows us to avoid proof orders in the correctness proof of completion. As a result, our proof is simpler than the one presented in textbooks, which is confirmed by our Isabelle/HOL formalization. Furthermore, we show that critical pair criteria are easily incorporated in our setting.

 

  PDF |    doi:10.1007/978-3-319-08970-6_19  |  © Springer International Publishing Switzerland

BibTeX 

@inproceedings{NHAMCS-ITP14,
author = "Nao Hirokawa and Aart Middeldorp and Christian Sternagel",
title = "A New and Formalized Proof of Abstract Completion",
booktitle = "Proceedings of the 5th International Conference on Interactive Theorem Proving",
editor = "Gerwin Klein and Ruben Gamboa",
series = "Lecture Notes in Computer Science",
volume = 8558,
pages = "292--307",
year = 2014,
doi = "10.1007/978-3-319-08970-6_19"
}
Nach oben scrollen