Acyclic logic programs and the completeness of SLDNF-resolution

AbstractThis paper investigates the class of acyclic programs, programs with the usual hierarchical condition imposed on ground instances of atoms rather than predicate symbols. The acyclic condition seems to naturally capture much of the recursion that occurs in practice and many programs that arise in practical programming satisfy this condition. We prove completeness of SLDNF-resolution for the acyclic programs and discuss several other desirable properties exhibited by programs belonging to this class