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.

BibTeX Entry

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