Decidability of Unification in the Theory of One-Sided Distributivity and a Multiplicative Unit

Unification in the equational theory of one-sided distributivity and a multiplicative unit is shown to be decidable. The algorithm is a non-deterministic one that eventually uses a decision algorithm for string unification problems with constant restrictions, which was shown to be decidable by K. Schulz extending the decision algorithm for string unification by Makanin.