The Undecidability of the $\mathrm{D}_\mathrm{A}$-Unification Problem
Siekmann, J. ; Szabo, P.
J. Symbolic Logic, Tome 54 (1989) no. 1, p. 402-414 / Harvested from Project Euclid
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.
Publié le : 1989-06-14
Classification: 
@article{1183742913,
     author = {Siekmann, J. and Szabo, P.},
     title = {The Undecidability of the $\mathrm{D}\_\mathrm{A}$-Unification Problem},
     journal = {J. Symbolic Logic},
     volume = {54},
     number = {1},
     year = {1989},
     pages = { 402-414},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183742913}
}
Siekmann, J.; Szabo, P. The Undecidability of the $\mathrm{D}_\mathrm{A}$-Unification Problem. J. Symbolic Logic, Tome 54 (1989) no. 1, pp.  402-414. http://gdmltest.u-ga.fr/item/1183742913/