The theory of first-order language where equality is the unique predicate symbol, which is known as the Free Equality Theory (abbreviated by FET), was introduced by Malcev and shown to be decidable by Maher and Comon&Lescanne. The Free Equality Theory is axiomatized by the usual equality axioms (reflexivity, symmetry, transitivity and compatibility), the classical unification axioms (decomposition, clash and occur-check) and the Domain Closure Axiom (DCA) (in the case of finite languages), which was first defined in Reiter for finite Herbrand domains. Besides, Compton&Henson and Vorobyov have proven that FET is non-elementary.
The problem of solving equality constraints without negation is known as unification and has been widely studied. However, unification problems lack of expressiveness since some equality constraints cannot
be transformed into a finite negation-free first order formula. Otherwise, if negation is allowed, then the problem is known as disunification or (general) equality constraint solving.
Most well-known algorithms for equality constraint solving are based on quantifier elimination. This method keeps formulas in some prenex normal form and iterates a procedure that, at each step, eliminates
the innermost block of existential/universal quantifiers of the prefix. Most of the decision methods for FET represent formulas in (particular cases of) disjunctive or conjunctive normal form, eliminating the innermost block of existential and universal quantifiers respectively. Regarding the first ones, the innermost block of existential quantifiers can be eliminated by simply removing all the equations/disequations involving their variables. However, when the innermost block is universal, double negation is applied in order to turn the block into existential. Hence, quantifier elimination methods require the transformation of formulas into normal form before and after the elimination of universal quantifiers.