On the Solvability of Equational Problems

Abstract

In this report we present some results on decidability, undecidability, semi-decidability, and non-semi-decidability of general and special equational problems. Solving an equational problem is the task to find out given an equational theory and any first order formula where the equality sign is the only predicate symbol, if this formula is true in the free algebra (or in the initial algebra) of this equational theory. One is usually interested in a constructive proof of an equational problem, i.e., the assignments of existentially quantified variables with elements of this algebra have to be constructed explicitely. Special cases are equality problems, unification and disunification problems: A disunification problem is the problem of solving a system of equations and disequations (i.e. negated equations) in the free or initial algebra of an equational theory, i.e. to prove the existentially closed conjunction of the equations and disequations in this algebra. Assignments for the variables occurring in the system, that make the terms of the equations equal, but let those of the disequations different are called solutions. Unification is as common the problem of solving a system of equations only, the solutions are called unifiers. Equality problems are universally closed equations. We are only interested in the question if there is a decision or at least a semi-decision procedure for the solvability of these problems but not in the task of finding procedures that compute the solutions.