摘要
Ｋｎｕｔｈ－Ｂｅｎｄｉｘ完备过程不终止的起因研究得很少．本文研究引起不终止的重写规则的结构性质，提出了相容交叉规则对的概念，推广了文献［６］的结论，并提出了为构造系统检验该过程是否不终止的方法．
Very little is known about the origin of nontermination of Knuth-Bendix completion procedure. In this paper, the structural properties of rewrite rules which cause nontermination are studied, the notion of compatible crossed rules is introduced. At last, a method for verifying nontermination of the procedure for constructive rewrite systems is provided.
出处
《计算机学报》
EI
CSCD
北大核心
1994年第6期464-468,共5页
Chinese Journal of Computers
基金
国家自然科学基金
