Depth-Bounded Inference for Nonterminating Prologs

Former version: Termination properties of a subclass of ground I/O logic programs, October,1990In this paper, we study the completeness of the depth-bounded resolution, which is an SLD-resolution that prunes infinite derivations using the depth-bound. We introduce a class of definite programs with local variables, called linearly covering programs, and prove the completeness of the depth-bounded resolution for the class with respect to the CWA of Reiter