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.
VAF-check (for Variant Atoms loop check for logic programs with Functions) was proposed by Shen @cite_14 . It is based on the notion of . VAF-check says that an SLD-derivation may be infinite if it generates an atomic subgoal @math that is an expanded variant of some of its ancestor @math , @math is a variant of @math except for some arguments @math such that: @math grows from @math to @math into a function containing @math , , @math grows from @math to @math into a function containing @math . VAF-check is as reliable as and more efficient than EVA-check @cite_14 .
@cite_14
1981314990
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.