A General Criterion for Avoiding Infinite Unfolding During Partial Deduction of Logic Programs.
Maurice Bruynooghe, Danny De Schreye, Bern Martens · Lirias · 1991
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.