On completeness of narrowing strategies

AbstractWe address the problem of unification modulo a set of equations, using the narrowing relation. We propose some syntactical criteria on algebraic specifications that ensure the completeness of narrowing strategies. We then prove a theorem relating narrowing and reduction relations. The completeness of narrowing strategies is proved and conditions for the computation of a “minimal” ground complete set of E-unifiers are given, as well as an algorithm transforming specifications satisfying Huet and Hullot's principle of definition into specifications fulfilling the proposed criteria