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"
}