LAZY NARROWING - STRONG COMPLETENESS AND EAGER VARIABLE ELIMINATION

Narrowing is an important method for solving unification problems in e quational theories that are presented by confluent term rewriting syst ems. Because narrowing is a rather complicated operation, several auth ors studied calculi in which narrowing is replaced by more simple infe rence rules. This paper is concerned with one such calculus. Contrary to what has been stated in the literature, we show that the calculus l acks strong completeness, so selection functions to cut down the searc h space are not applicable. We prove completeness of the calculus and we establish an interesting connection between its strong completeness and the completeness of basic narrowing. We also address the eager va riable elimination problem. It is known that many redundant derivation s can be avoided if the variable elimination rule, one of the inferenc e rules of our calculus, is given precedence over the other inference rules. We prove the completeness of a restricted variant of eager vari able elimination in the case of orthogonal term rewriting systems.