A Dynamic Approach to Characterizing Termination of General Logic Programs

TL;DR

This paper introduces a dynamic method for analyzing the termination of general logic programs by utilizing features of derivations and a new generalized SLDNF-tree structure, contrasting with traditional static approaches.

Contribution

It proposes a novel dynamic approach and a new formulation of SLDNF-trees for better termination analysis of logic programs.

Findings

Dynamic features like subgoal repetition are effective for termination characterization.

Generalized SLDNF-trees handle negative subgoals similarly to Prolog.

The approach applies to any general logic program.

Abstract

We present a new characterization of termination of general logic programs. Most existing termination analysis approaches rely on some static information about the structure of the source code of a logic program, such as modes/types, norms/level mappings, models/interargument relations, and the like. We propose a dynamic approach which employs some key dynamic features of an infinite (generalized) SLDNF-derivation, such as repetition of selected subgoals and recursive increase in term size. We also introduce a new formulation of SLDNF-trees, called generalized SLDNF-trees. Generalized SLDNF-trees deal with negative subgoals in the same way as Prolog and exist for any general logic programs.