On the termination of an algorithm for unification in equational theories

The termination properties of a semantic unification procedure for the problem t=_Rt´ are studied, where R is expressed by means of a canonical term rewriting system and t´ is a round term not containing any defined function symbol. The procedure is shown to be terminating whenever R satisfies a condition whose main point is the `strictly conicity´ of the recursive right hand side of the rules. Moreover, the necessity of such a condition is shown for a suitable class of term rewriting systems and equations