Title: A completeness theorem for SLDNF resolution
Abstract: We prove the completeness of SLDNF resolution and negation as failure for stratified, normal programs and normal goals, under the conditions of strickness and allowedness. In particular, this result settles positively a conjecture of Apt, Blair, and Walker.