A class of programs for which SLDNF resolution and NAF rule are complete