Termination analysis for tabled logic programming

© Springer-Verlag Berlin Heidelberg 1998. We provide a theoretical basis for studying the termination of tabled logic programs executed under SLG-resolution using a leftto-right computation rule. To this end, we study the classes of quasi-terminating and LG-terminating programs (for a set of atomic goals S). These are tabled logic programs where execution of each call from S leads to only a nite number of dierent (i.e., non-variant) calls, and a nite number of dierent calls and computed answer substitutions for them, respectively. We then relate these two classes through a program transformation, and present a characterisation of quasi-termination by means of the notion of quasi-acceptability of tabled programs. The latter provides us with a practical method of proving termination and the method is illustrated on non-trivial examples of tabled logic programs.status: publishe