Termination Analysis for Tabled Logic Programming

We provide a theoretical basis for studying the termination of tabled logic programs executed under SLG-resolution using a left-to-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 finite number of different (i.e., non-variant) calls, and a finite number of different 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.