The termination properties of a semantic unification procedure for the problem t=/sub R/t' 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.
展开▼
机译：研究了问题t = / sub r / t'的语义统一过程的终止特性，其中通过规范术语重写系统而表示，T'是不包含任何定义的函数符号的圆术语。只要r满足一个条件，该过程将终止终止，其主要点是规则的递归右侧的“严格圆角”的条件。此外，示出了适当的术语重写系统和方程类别的这种情况的必要性。
展开▼
