Completeness and Termination of SLDNF-Resolution and Determination of a Selection function using Mode

We consider a mode of an n-ary predicate symbol with respect to a logic program, which meets the aim of logic programming and captures the spirit of unification as arguments passing mechanism. We prove that the SLDNF-resolution which resolves a non-ground negative literal is complete for an interesting class of logic programs using this mode. To obviously do such a proof we do consider terms modulo variable renaming and map a logic program with a goal to an allowed logic program with an allowed goal, since it is well-known that the SLDNF-resolution is complete for the class of allowed logic programs with allowed goals [Kunen89]. The termination of the SLDNF-resolution is studied using a sophisticated selection function which only chooses those literals and clauses that are applicable in the sense that using such literals and clauses the SLDNF-resolution would not be infinite, if a finite SLDNF-resolution does exist