Narrowing vs. SLD-resolution

AbstractA comparison is performed between narrowing and SLD-resolution as regards their use in semantic unification (or E-unification). An E-unification algorithm based on flattening and SLD-resolution is developed and proved sound and complete by establishing a correspondence between narrowing sequences and resolution sequences. An E-unification algorithm based on a refined (“selection”) narrowing strategy is derived by adapting the SLD-strategy to narrowing. Finally, possible applications to the domain of logic+functional programming are considered