Left-Linear Completion with AC Axioms
<|reference_start|>Left-Linear Completion with AC Axioms: 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.<|reference_end|>
@article{niederhauser2024left-linear,
    title={Left-Linear Completion with AC Axioms},
    author={Johannes Niederhauser, Nao Hirokawa and Aart Middeldorp},
    journal={arXiv preprint arXiv:2405.17109},
    year={2024},
    archivePrefix={arXiv},
    eprint={2405.17109},
    primaryClass={cs.LO}
}