Termination of logic programs with delay declarations

This paper proposes 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 with respect to an arbitrary selection rule. Most importantly, we use the notion of bounded 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 focal 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. (C) 1999 Elsevier Science Inc. All rights reserved.