Since the seminal work of J. A. Robinson on resolution, many lifting lemmas for simplifying proofs of completeness of resolution have been proposed in the literature. In the logic programming framework, they may also help to detect some infinite derivations while proving goals under the SLD-resolution. In this paper, we first generalize a version of the lifting lemma, by extending the relation "is more general than" so that it takes into account only some arguments of the atoms. The other arguments, which we call neutral arguments, are disregarded. Then we propose two syntactic conditions of increasing power for identifying neutral arguments from mere inspection of the text of a logic program.
 Two complete loop checking mechanisms have been presented in the literature for logic programs with functions: OS-check and EVA-check. OS-check is computationally efficient but quite unreliable in that it often misidentifies infinite loops, whereas EVA-check is reliable for a majority of cases but quite expensive. In this paper, we develop a series of new complete loop checking mechanisms, called VAF-checks. The key technique we introduce is the notion of expanded variants, which captures a key structural characteristic of in finite loops. We show that our approach is superior to both OS-check and EVA-check in that it is as efficient as OS-check and as reliable as EVA-check. Copyright 2001 Elsevier Science B.V. The Equality check and the Subsumption check are weakly sound, but are not complete even for function-free logic programs. Although the OverSize (OS) check is complete for positive logic programs, it is too general in the sense that it prunes SLD-derivations merely based on the depth-bound of repeated predicate symbols and the size of atoms, regardless of the inner structure of the atoms, so it may make wrong conclusions even for some simple programs. In this paper, we explore complete loop checking mechanisms for positive logic programs. We develop an extended Variant of Atoms (VA) check that has the following features: (1) it generalizes the concept of “variant” from “the same up to variable renaming” to “the same up to variable renaming except possibly with some arguments whose size recursively increases”, (2) it makes use of the depth-bound of repeated variants of atoms instead of depth-bound of repeated predicate symbols, (3) it combines the Equality Subsumption check with the VA check, (4) it is complete w. r. t. the leftmost selection rule for positive logic programs, and (5) it is more sound than both the OS check and all the existing versions of the VA check.