2026-08-13T18:49:04Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:7725 2024-03-06T10:41:03Z ddc:004 open_access

Infinite Runs in Abstract Completion Hirokawa, Nao Middeldorp, Aart Sternagel, Christian Winkler, Sarah term rewriting abstract completion ordered completion canonicity Isabelle/HOL 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Nao Hirokawa and Aart Middeldorp and Christian Sternagel and Sarah Winkler 2017 Is Part Of LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2017.19 urn:nbn:de:0030-drops-77252 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.19 eng https://creativecommons.org/licenses/by/3.0/legalcode