Journal of Logic and Computation, Volume 9, Issue 1, pp. 47-61: Abstract.
A direct proof of the completeness of SLDNF-resolution
Institute of Informatics, University of Fribourg, Rue Faucigny 2, CH-1700 Fribourg, Switzerland. E-mail: email@example.com
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, non-floundering SLDNF-tree 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, non-ground literals only.
Key words: Logic programming, negation as failure, SLDNF-resolution.