Johannes Niederhauser, Nao Hirokawa, Aart Middeldorp
Proceedings of the 29th International Conference on Automata Deduction (CADE-29), Lecture Notes in Artificial Intelligence 14132, pp. 401-418, 2023
pdf 
doi:10.1007/978-3-031-38499-8_27
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 tool accompll.
BibTex
@inproceedings{JNNHAM-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"}