Left-Linear Completion with AC Axioms
Johannes Niederhauser, Nao Hirokawa and Aart Middeldorp
Proceedings of the 29th International Conference on Automated Deduction
(CADE-29), Lecture Notes in Artificial Intelligence 14132,
pp. 401 – 418, 2023
Abstract
We revisit AC completion for left-linear term rewrite systems where AC unification 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. 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. Finally, we present experimental results for our implementation of left-linear AC completion in the toolaccompll.
BibTeX Entry
@inproceedings{NHM-CADE23,
author = "Johannes Niederhauser and Nao Hirokawa and Aart Middeldorp",
title = "Left-Linear Completion with {AC} Axioms",
booktitle = "Proceedings of the 29th International Conference on Automated
Deduction",
editor = "Brigitte Pientka and Cesare Tinelli",
series = "Lecture Notes in Artificial Intelligence",
volume = 14132,
pages = "401--418",
year = 2023,
doi = "10.1007/978-3-031-38499-8\_23"
}