Abstract

We show that the $\mathrm{D_A}$-unification problem is undecidable. That is, given two binary function symbols $\bigoplus$ and $\bigotimes$, variables and constants, it is undecidable if two terms built from these symbols can be unified provided the following $\mathrm{D_A}$-axioms hold: \begin{align*}(x \bigoplus y) \bigotimes z &= (x \bigotimes z) \bigoplus (y \bigotimes z),\\x \bigotimes (y \bigoplus z) &= (x \bigotimes y) \bigoplus (x \bigotimes z),\\x \bigoplus (y \bigoplus z) &= (x \bigoplus y) \bigoplus z.\end{align*} Two terms are $\mathrm{D_A}$-unifiable (i.e. an equation is solvable in $\mathrm{D_A}$) if there exist terms to be substituted for their variables such that the resulting terms are equal in the equational theory $\mathrm{D_A}$. This is the smallest currently known axiomatic subset of Hilbert's tenth problem for which an undecidability result has been obtained