TUTORIAL ON TERMINATION OF LOGIC PROGRAMS

We present a general introduction to termination analysis for logic programs, with focus on universal termination of SLD-derivations and on definite programs. We start by providing a generic definition of the termination problem. It is parametrised by the sets of goals and the sets of computation rules under consideration. We point out a distinction between two streams of work, each taking a different approach with respect to the undecidability of the halting problem. We then recall the notions of recurrency and acceptability from the works of Apt, Bezem and Pedreschi. We illustrate how these notions provide an elegant framework for reasoning about termination. We then identify four basic components that are present in any approach to termination analysis. We point out the interdependencies between these components and their relevance for the termination analysis as a whole. We also use these components to illustrate some differences between automatic approaches to termination analysis and the more theoretically oriented frameworks for termination.