The Undecidability of the [D A]-Unification Problem

Abstract

We show that the DA-Unification problem is undecidable. That is, given two binary function symbols Φ and Θ, variables and constants, it is undecidable if two terms built from these symbols can be unified provided the following DA-axioms hold: (x Φ y) Θ z = (x Θ z) Φ (y Θ z) x Θ (y Φ z) = (x Θ y) Φ (x Θ z) x Φ (y Φ z) = (x Φ y) Φ z Two terms are DA-unifiable (i.e. an equation is solvable in DA) if there exist terms to be substituted for their variables such that the resulting terms are equal in the equational theory DA. This is the smallest currently known axiomatic subset of Hilbert's Tenth Problem for which an undecidability result has been obtained.