Complete axiomatizations of some quotient term algebras

We show that T(F)/ =_E can be completely axiomatized when =_E is a quasi-free theory. Quasi-free theories are a wider class of theories than permutative theories of [Mal71] for which Mal'cev gave decision results. As an example of application, we show that the first order theory of T(F)/ =_E is decidable when E is a set of ground equations. Besides, we prove that the ∑₁-fragment of the theory of T(F)/ =_E is decidable when E is acompact set of axioms. In particular, the existential fragment of the theory of associative-commutative function symbols is decidable.