Bounded ACh Unification

Ajay Kumar Eeralla, Christopher Lynch

We consider the problem of the unification modulo an equational theory ACh, which consists of a function symbol $h$ that is homomorphic over an associative-commutative operator $+$…