LOOP CHECKING IN PARTIAL DEDUCTION

In the framework of Lloyd and Shepherdson [16], partial deduction involves the creation of SLDNF-trees for a given program and some goals up to certain halting points. This paper identifies the relation between halting criteria for partial deduction and loop checking (as formalized in [1]). For simplicity, we consider only positive programs and SLD-resolution here. It appears that loop checks for partial deduction must be complete, whereas traditionally, the soundness of a loop check is more important. However, it is also shown that sound loop checks can contribute to improve partial deduction. Finally, a class of complete loop checks suitable for partial deduction is identified.