Thank you Dexter. I understand that you suggest that I should redefine most basic notions that I need from the start to avoid the terminology problem. I will do so. However there is a big risk that some reviewers critisize the fact that I do not stick to standard terminology. I have some trouble with this notion of a ground equation, especially when the equation contains "uninterpreted constants", which, in my understanding, are the same thing as "universally quantified variables".

The word algebra here is used more generally for an arbitrary signature. A finitely presented algebra is defined by a pair <G, R> where G is a finite set of "generators" et R is a finite set of pairs of terms built from the generators and the function symbols of the algebra.