Journal of Logic and Computation, Volume 9, Issue 1, pp. 4761: Abstract.
A direct proof of the completeness of SLDNFresolutionR Stärk Institute of Informatics, University of Fribourg, Rue Faucigny 2, CH1700 Fribourg, Switzerland. Email: robert.staerk@unifr.ch
We give a direct proof of the following theorem: if a goal G[sgr] is a logical consequence of the partial completion of an arbitrary normal logic program P, then each fair, nonfloundering SLDNFtree T for G yields an answer substitution &thgr which is more general than [sgr]. If the negation G is a logical consequence of the partial completion of P, then T is finitely failed. A tree is fair, if each negative main branch ends in failure or each literal in the branch is selected at a certain point. A tree is floundering if it contains a positive node that consists of negative, nonground literals only. Key words: Logic programming, negation as failure, SLDNFresolution.
