Nao Hirokawa ; Aart Middeldorp ; Christian Sternagel ; Sarah Winkler - Abstract Completion, Formalized

lmcs:4314 - Logical Methods in Computer Science, August 21, 2019, Volume 15, Issue 3 - https://doi.org/10.23638/LMCS-15(3:19)2019
Abstract Completion, Formalized

Authors: Nao Hirokawa ; Aart Middeldorp ; Christian Sternagel ; Sarah Winkler

    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├ętivier concerning canonicity of rewrite systems. All proofs presented in the paper have been formalized in Isabelle/HOL.


    Volume: Volume 15, Issue 3
    Published on: August 21, 2019
    Accepted on: August 21, 2019
    Submitted on: February 26, 2018
    Keywords: Computer Science - Logic in Computer Science
    Fundings :
      Source : OpenAIRE Research Graph
    • Certification Redux; Funder: Austrian Science Fund (FWF); Code: P 27502
    • From Confluence to Unique Normal Forms: Certification and Complexity; Funder: Austrian Science Fund (FWF); Code: P 27528
    • Instantiation- and Learning-Based Methods in Equational Reasoning; Funder: Austrian Science Fund (FWF); Code: T 789

    Share

    Consultation statistics

    This page has been seen 539 times.
    This article's PDF has been downloaded 292 times.