A Generalization of the Lifting Lemma for Logic Programming

TL;DR

This paper generalizes the lifting lemma in logic programming by introducing neutral arguments, aiding in detecting infinite derivations and improving proof completeness analysis.

Contribution

It extends the lifting lemma to consider only certain arguments, and proposes syntactic conditions to identify neutral arguments in logic programs.

Findings

Extended the lifting lemma to include neutral arguments.

Proposed syntactic criteria for identifying neutral arguments.

Enhanced methods for detecting infinite derivations.

Abstract

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.