Higher-order lazy narrowing is a general method for solving E-unification problems in theories presented as sets of rewrite rules. In this paper we study the possibility of improving the search for normalized solutions of a higher-order lazy narrowing calculus LN. We introduce a new calculus, LN_(ff), obtained by extending LN and define an equation selection strategy S_n such that LN_(ff) with strategy S_n is comlete. The main advantages of using LN_(ff) with strategy S_n instead of LN include the possibility of restricting the application of outermost narrowing at variable position, and the computation of more specific solutions because of additional inference rules for solving flex-flex equations. We also show that for orthogonal pattern rewrite systems we can adopt an eager variable elimination strategy that makes the calculus LN_(ff) with strategy S_n even more deterministic.
展开▼
