Generalizing completeness results for loop checks in logic programming (Q1199926)

Loop checking is one of the fundamental problems encountered during the search of effective algorithms for logic programming. This complex problem cannot be solved in full generality (even in absence of function symbols). In \textit{R. N. Bol, K. R. Apt} and \textit{J. W. Klop} [ Theor. Comput. Sci. 86, No. 1, 35-79 (1991; Zbl 0741.68027)], (sound) loop checks were introduced and there were determined subclasses of programs for which these checks are complete. The Generalization Theorem of the present paper presents a method to extend these subclasses under certain natural conditions. A crucial role in this approach plays the notion of nonrecursive extension of a logic program. The proof itself calls attention to normal SLD derivations which put extra requirements on the used most general unifiers (limiting needless renaming of variables in a derivation).