Completeness Result of SLDNF-resolution for a relevant Class of Logic Programs

The proof theory of logic programming has been given by the SLDNF-resolution which has been proven complete for the class of arbitrary logic programs when assuming fair selection and non-floundering [Drabent96,Staerk97]. To test the non-floundering condition is as hard as to resolve the problem itself. To overcome this assumption we first of all extend the universe to one that contains variables modulo renaming and define the bottom up SLDNF-resolution so that the elimination of this assumption is obvious. We then prove that the so defined SLDNF-resolution is sound and complete for a larger class of logic programs which does obviously contain the classes mentioned above