Johannes Niederhauser ; Nao Hirokawa ; Aart Middeldorp - Left-Linear Completion with AC Axioms

lmcs:13670 - Logical Methods in Computer Science, April 29, 2025, Volume 21, Issue 2 - https://doi.org/10.46298/lmcs-21(2:10)2025
Left-Linear Completion with AC AxiomsArticle

Authors: Johannes Niederhauser ; Nao Hirokawa ; Aart Middeldorp

    We revisit completion modulo equational theories for left-linear term rewrite systems where unification modulo the theory is avoided and the normal rewrite relation can be used in order to decide validity questions. To that end, we give a new correctness proof for finite runs and establish a simulation result between the two inference systems known from the literature. Given a concrete reduction order, novel canonicity results show that the resulting complete systems are unique up to the representation of their rules' right-hand sides. Furthermore, we show how left-linear AC completion can be simulated by general AC completion. In particular, this result allows us to switch from the former to the latter at any point during a completion process.


    Volume: Volume 21, Issue 2
    Published on: April 29, 2025
    Accepted on: February 28, 2025
    Submitted on: May 28, 2024
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 264 times.
    This article's PDF has been downloaded 124 times.