Click on the title to obtain a gzip-ed PostScript version of the paper (95K).
Abstract:
Tabling avoids many of the shortcomings of SLD(NF) execution and
provides a more flexible and efficient execution mechanism for logic
programs. In particular, tabled execution of logic programs
terminates more often than execution based on SLD-resolution. One
of the few works studying termination under s tabled execution
mechanism is that of Decorte et al.
They introduce and characterise two notions of universal termination
of logic programs w.r.t. sets of queries executed under SLG-resolution,
using the left-to-right selection rule; namely the notion of
quasi-termination and the (stronger) notion of LG-termination.
This paper extends the results of Decorte et al in two
ways:
- we consider a mix of tabled and Prolog execution, and
- besides a characterisation of the two notions of universal
termination under such a mixed execution, we also give modular
termination conditions.
From both practical and efficiency
considerations, it is important to allow tabled and non-tabled
predicates to be freely intermixed. This motivates the first
extension. Concerning the second extension, it was already noted in
the literature in the context of termination under SLD-resolution
(by e.g. Apt and Pedreschi), that it is important for programming in
the large to have modular termination proofs, i.e. proofs that are
capable of combining termination proofs of separate programs to
obtain termination proofs of combined programs.