A strategy to deal with divergent rewrite systems

In this paper a new approach to divergence in Knuth-Bendix completion is presented. Given a term rewriting system R, whose completion diverges, a strategy can be defined to simulate the applicalion of the (infinitely many) rewrite rules derived from critical pairs without attempting any completion. This is done by applying some of the rules in R also as expansion rules.