Loop checking in SLD-derivations by well-quasi-ordering of goals

Loop checking mechanisms are used to detect and prune infinite SLD derivati ons, through run time checks which are introduced in logic program interpre ters. Simple loop checks, i.e, checks which do not depend on the specific l ogic program, have been widely studied in literature. Since no sound and co mplete loop check exists even in the case of function-free programs, severa l subclasses have been characterized for which sound and complete loop chec ks can be determined. In this paper a theoretical framework for analysing p roperties of loop check mechanisms for logic programs is proposed, which ex ploits general mathematical results about well-quasi-ordered (wqo) sets. In a way, the method can be viewed as a counterpart of well known techniques based on well-founded partial-ordering, used in termination proofs for rewr iting systems and for logic programs. The main results are obtained on the basis of a combinatorial analysis of properties of wqo sets of goals. As sh own in the paper, subclasses of programs, for which sound and complete simp le loop checks exist, can be easily framed in the wqo approach. Reasons for the different behaviours of subsumption loop checks based on list and mult iset goal comparisons are also plainly highlighted. (C) 2000 Elsevier Scien ce B.V. All rights reserved.