Syntactic theories and unification

An investigation is made of the relationship between unifiability of a general equation of the form f(ν₁, . . ., ν_n)=^?g(ν_n+1, . . ., ν _m), and of the syntacticness of the theory. After introducing the concept of general equations and its basic properties, the precise definition of syntactic theories is given. It is proven that a theory is syntactic if and only is the general equations have finite complete set of E-solutions. The result is constructive in the sense that from the E-solutions of the general equations, a resolvent presentation is computed. This is applied to several theories: in particular, in order to show that distributivity is not syntactic. The authors also prove that the theory of associativity and commutativity is syntactic, which allows one, by the combination of Nipkow´s results (ibid., p.278-88, 1990) and the authors´, to infer a novel matching algorithm where there is no need to solve linear diophantine equations