Abstract

Completion is one of the first and most studied techniques in term rewriting and fundamental to automated reasoning with equalities. In an earlier paper we presented a new and formalized correctness proof of abstract completion for finite runs. In this paper we extend our analysis and our formalization to infinite runs, resulting in a new proof that fair infinite runs produce complete presentations of the initial equations. We further consider ordered completion – an important extension of completion that aims to produce ground-complete presentations of the initial equations. Moreover, we revisit and extend results of Métivier concerning canonicity of rewrite systems. All proofs presented in the paper have been formalized in Isabelle/HOL.

BibTeX Entry

@inproceedings{HMSW-FSCD17,
 author    = "Nao Hirokawa and Aart Middeldorp and Christian Sternagel and
              Sarah Winkler",
 title     = "Infinite Runs in Abstract Completion",
 booktitle = "Proceedings of the 2nd International Conference on Formal
              Structures for Computation and Deduction",
 editor    = "Dale Miller",
 series    = "Leibniz International Proceedings in Informatics"
 volume    = 84,
 pages     = "19:1--19:16",
 year      = 2017,
 doi       = "10.4230/LIPIcs.FSCD.2017.19"
}