Improving basic narrowing techniques

Abstract

In this paper, we propose a new and complete method based on narrowing for solving equations in equational theories. It is a combination of basic narrowing and narrowing with eager reduction, which is not obvious, because their naive combination is not a complete method. We show that it is more efficient than the existing methods in many cases, and for that establish commutation properties on the narrowing. It provides an algorithm that has been implemented as an extension of the REVE software.