New generation computing vol:11 issue:1 pages:47-79
Well-founded orderings are a commonly used tool for proving the termination of programs. We introduce related concepts specialised to SLD-trees- Based on these concepts, we formulate formal and practical criteria 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 provides both a formal and practically applicable framework.