Completeness of Depth-Bounded Resolution for Weakly Reducing Programs

World Scientific Series in Computer Science, 31, 227--245,1991SLDNF-resolution procedure is not complete with respect to the perfect model semantics for logic programs in general. In this paper, sve introduce two classes of logic programs containing function symbols, reducing programs and weakly reducing programs, which are characterized by the size of atom. For these classes of programs, we prove the completeness of the derivation procedure which makes use of depth-bound. First, we introduce the local finiteness of Herbrand base of a program, and prove the finite fixpoint property for the class of programs which satisfies the local finiteness. Further, we show that the class of weakly reducing programs, a subclass of locally stratified programs, has some syntactic conditions, and prove that it has the finite fixpoint property. Using the finite fixpoint property, we prove the completeness of depth-bounded derivations for weakly reducing programs. In particular, we prove the completeness of unbounded derivations for reducing programs