Acyclic logic programs and the completeness of SLDNF-resolution (Q1177925)

The paper investigates the class of acyclic logic programs, which is a subclass of the locally hierarchical programs defined by imposing the condition, that every ground atom is assigned a finite level. The class of locally hierarchical programs generalizes that of the hierarchical programs by imposing the hierarchical constraints on ground instances of atoms rather than on predicate symbols. The SLDNF-resolution for locally hierarchical programs is not complete but for acyclic programs the completeness is proved. Several other desirable properties exhibited by programs belonging to this class are discussed.