Infinite Runs in Abstract Completion
Nao Hirokawa, Aart Middeldorp, Sarah Winkler, and Christian SternagelProceedings of the 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), Leibniz International Proceedings in Informatics 84, pp. 19:1 – 19:16, 2017.
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
@inproceedings{NHAMSWCS-FSCD17, author = "Nao Hirokawa and Aart Middeldorp and Sarah Winkler and Christian Sternagel", title = "Infinite Runs in Abstract Completion", booktitle = "Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)", 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" }