A general criterion for avoiding infinite unfolding during partial deduction of logic programs

Well-founded orderings are a commonly used tool for proving the termination of programs. We introduce related concepts specialized 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 that 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.status: publishe