A GENERAL CRITERION FOR AVOIDING INFINITE UNFOLDING DURING PARTIAL DEDUCTION

Well-founded orderings are a commonly used tool for proving the termin ation of programs. We introduce related concepts specialised to SLD-tr ees- Based on these concepts, we formulate formal and practical criter ia for controlling the unfolding during the construction of SLD-trees that form the basis of a partial deduction. We provide algorithms thaL allow to use these criteria in a constructive way. In contrast to the many ad hoc techniques proposed in the literature, our technique prov ides both a formal and practically applicable framework.