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.
|Logic Programming (acm D.1.6), Software/Program Verification (acm D.2.4), Specifying and Verifying and Reasoning about Programs (acm F.3.1)|
|Logic programming (msc 68N17), Complexity classes (hierarchies, relations among complexity classes, etc.) (msc 68Q15), Theory of computing (msc 68Qxx), Specification and verification (program logics, model checking, etc.) (msc 68Q60)|
|Department of Computer Science [CS]|
Marchiori, E, & Teusink, F. J. M. (1996). Proving termination of logic programs with delay declarations. Department of Computer Science [CS]. CWI.