Click on the title to obtain a gzip-ed PostScript version of the paper (63K).
Abstract:
We provide a theoretical basis for studying the termination of tabled
logic programs executed under SLG-resolution using a left-to-right
selection 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.