S. Verbaeten et D. De Schreye, Termination of simply-moded well-typed logic programs under a tabled execution mechanism, APPL ALG EN, 12(1-2), 2001, pp. 157-196
Citations number
32
Categorie Soggetti
Engineering Mathematics
Journal title
APPLICABLE ALGEBRA IN ENGINEERING COMMUNICATION AND COMPUTING
Tabled logic programming is receiving increasing attention in the Logic Pro
gramming community. It avoids many of the shortcomings of SLD(NF) execution
and provides a more flexible and often extremely efficient execution mecha
nism for logic programs. In particular, tabled execution of logic programs
terminates more often than execution based on SLD-resolution. So, if a prog
ram can be proven to terminate under SLD-resolution, then the program will
trivially also terminate under SLG-resolution, the resolution principle of
tabling. But, since there are SLG-terminating programs which are not SLD-te
rminating, more effective proof techniques can be found. One of the few app
roaches studying termination of tabled logic programs was developed by Deco
rte et al. They present necessary and sufficient conditions for two notions
of termination under LG-resolution, i.e. SLG-resolution with left-to-right
selection rule: quasi-termination and (the stronger notion of) LG-terminat
ion. Starting from these necessary and sufficient conditions, we introduce
sufficient conditions for quasi-termination and LG-termination which are st
ated fully at the clause level and are easy to automatize. To this end, we
use mode and type information: we consider simply-moded, well-typed program
s and queries. We point out how our termination conditions can be automatiz
ed, by extending the recently developed, constraint-based, automatic termin
ation analysis for SLD-resolution of Decorte and De Schreye. Finally, we pr
esent a result on substitution-closedness of quasi-termination and LG-termi
nation for the class of simply-moded, well-typed programs and queries.