Proving termination of logic programs with delay declarations

In this paper we propose a method for proving termination of logic programs with delay declarations. The method is based on the notion of recurrent logic program, which is used to prove programs terminating wrt an arbitrary selection rule. Most importantly, we use the notion of bound query (as proposed by M. Bezem) in the definition of cover, a new notion which forms the kernel of our approach. We introduce the class of delay recurrent programs and prove that programs in this class terminate for all local delay selection rules, provided that the delay conditions imply boundedness. The corresponding method can be also used to transform a logic program into a terminating logic program with delay declarations.