Solving *-problems modulo Distributivity by a Reduction to AC1-unification

Abstract: We show that unification modulo both-sided distributivity of the symbol * on + can be reduced to AC1-unification for all unification problems which do not involve the + operator. Moreover, in this case, we can describe “almost all” solutions in a finite way, although there are in general infinitely many minimal solutions for such problems.

This document was translated from L^AT_EX by H^EV^EA.