Soundness and Completeness versus Lifting Property

. We give new formulations of the property of soundness and completeness of a resolution system and of the lifting lemma, and we discuss their relationship. The discussion points out why certain resolution systems are not complete, and that there is a simple method for showing that a resolution system is "absolutely incomplete" -- that there is no notion of program completion and no logic which could give soundness and completeness. The method is demonstrated on the case of basic variants of the SLDNF-resolution. The same approach can be used to analyze other resolution systems. Keywords: soundness and completeness, lifting lemma, program completion, SLDNF-resolution. 1 Introduction One of the ideas underlying the development of logic programming is that programming should be to a greater extent declarative. Declarativeness of logic programming is characterized in a formal way, by so called, soundness and completeness properties. Many sound resolution systems have been proposed as po..