## A partial solution for |

Abstract:We show that deciding unification modulo both-sided distributivity of a symbol * over a symbol + can be reduced toAC1-unification for all unification problems which do not involve the + operator. Moreover, we can describe “almost all” solutions in a finite way, although there are in general infinitely many minimal solutions for such problems. As a consequence, *-problems appear as a good candidate for a notion of solved-form forD-unification.

This document was translated from L^{A}T_{E}X byH^{E}V^{E}A.