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

TL;DR

This paper introduces a new dynamic method for analyzing the termination of general logic programs with moded queries, capable of testing termination for specific, all, or most queries, enhancing the understanding of program behavior.

Contribution

It presents a novel dynamic approach to termination analysis for logic programs with moded queries, including formulation, characterization, and loop checking techniques.

Findings

Effective in testing termination for specific queries

Can determine termination for all possible queries

Identifies most general queries likely to terminate or not

Abstract

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).