| ||||
| ||||
![]() Title:Left-Linear Completion with AC Axioms Conference:CADE-29 Tags:AC axioms, Completion and Term rewriting 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 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. Left-Linear Completion with AC Axioms ![]() Left-Linear Completion with AC Axioms | ||||
Copyright © 2002 – 2025 EasyChair |