  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.
