Completeness of Dynamic Time-Bounded Derivation for Locally Weak Reducing Programs

In the logic programming, it is generally undecidable, whether or not a formula is deducible from a program. In this paper, we discuss the relations between structure of programs and termination of derivations, and show that the predicate symbols in a program can be classified and stratified by a relation between them. We propose two classes of logic programs called locally weak reducing and locally reducing programs. We also give a new dynamic time-bounded derivation procedure, and prove the completeness of this procedure for locally weak reducing programs