Abstract Completion, Formalized

TL;DR

This paper provides new correctness proofs for abstract and ordered completion techniques in term rewriting, including formalization in Isabelle/HOL, enhancing understanding of their completeness and canonicity.

Contribution

It introduces novel correctness proofs for finite and infinite runs of abstract completion, extends results to ordered completion, and formalizes all proofs in Isabelle/HOL.

Findings

Correctness proofs for finite and infinite abstract completion runs

New proof for ground completion based on random descent

Extended results on the completeness and canonicity of ordered completion

Abstract

Completion is one of the most studied techniques in term rewriting and fundamental to automated reasoning with equalities. In this paper we present new correctness proofs of abstract completion, both for finite and infinite runs. For the special case of ground completion we present a new proof based on random descent. We moreover extend the results to ordered completion, an important extension of completion that aims to produce ground-complete presentations of the initial equations. We present new proofs concerning the completeness of ordered completion for two settings. Moreover, we revisit and extend results of M\'etivier concerning canonicity of rewrite systems. All proofs presented in the paper have been formalized in Isabelle/HOL.