2 papers
cs.LO2025
Hydra Battles and AC Termination
Nao Hirokawa, Aart Middeldorp
We present a new encoding of the Battle of Hercules and Hydra as a rewrite system with AC symbols. Unlike earlier term rewriting encodings, it faithfully models any strategy of Her…
cs.LO2025
Left-Linear Completion with AC Axioms
Johannes Niederhauser, Nao Hirokawa, Aart Middeldorp
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…