The undecidability of the DA-Unification problem

Journal of Symbolic Logic 54 (2):402 - 414 (1989)
  Copy   BIBTEX


We show that the 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 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 D A -unifiable (i.e. an equation is solvable in D A ) if there exist terms to be substituted for their variables such that the resulting terms are equal in the equational theory D A . This is the smallest currently known axiomatic subset of Hilbert's tenth problem for which an undecidability result has been obtained



    Upload a copy of this work     Papers currently archived: 92,323

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library


Added to PP

34 (#473,178)

6 months
9 (#317,960)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations