A partial solution for D-unification based on a reduction to AC1-unification

. We show that deciding unification modulo both-sided distributivity of a symbol over a symbol + can be reduced to AC1- 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 for D-unification. 1 Introduction Equations are ubiquitous in mathematics as well as in computer science. Unification is solving equations in some particular domains, namely free term algebras or term algebras modulo an equational theory. Unification was first introduced by Herbrand [3], and rediscovered by Robinson as a basic mechanism for resolution in first order logic [10]. Unification is also the basic mechanism for computing critical pairs [7], and the main inference rule of the completion procedure. On the other hand, the very old and famous 10 th Hilb..