On nontermination of Knuth-Bendix algorithm

Abstract

The well-known Knuth-Bendix completion algorithm which computes a confluent and finitely terminating term rewriting system from a given set of equations, can either terminate with success or abort or even nonterminate. Very little is known about the origin of nontermination of this algorithm. We study the structural properties of rewrite rules which cause nontermination. The notion of the crossed rules is introduced for these purposes. We look for sufficient conditions guaranteeing nontermination of algorithm in the presence of crossed rules. A special attention is devoted to a verifiable condition of such kind.