Termination Analysis of General Logic Programs for Moded Queries: A Dynamic Approach

The termination problem of a logic program can be addressed in either a static or a dynamic way. A static approach performs termination analysis at compile time, while a dynamic approach characterizes and tests termination of a logic program by applying a loop checking technique. In this paper, we present a novel dynamic approach to termination analysis for general logic programs with moded queries. We address several interesting questions, including how to formulate an SLDNF-derivation for a moded query, how to characterize an infinite SLDNF-derivation with a moded query, and how to apply a loop checking mechanism to cut infinite SLDNF-derivations for the purpose of termination analysis. The proposed approach is very powerful and useful. It can be used (1) to test if a logic program terminates for a given concrete or moded query, (2) to test if a logic program terminates for all concrete or moded queries, and (3) to find all (most general) concrete/moded queries that are most likely terminating (or non-terminating).