Analyzing the termination of programs is perhaps one of the most active research topics in most declarative programming languages. Within the logic programming paradigm, one can find two different types of approaches to analyze termination: direct approaches that deal with logic programs without any preprocessing, and transformational approaches that first transform them to term rewriting systems, and then analyze the termination of these systems. The transformational approach is particularly interesting, because it allows one to reuse the huge body of techniques and tools for analyzing the termination of term rewriting systems, perhaps the one setting where a lot of effort has been devoted to this kind of research.

In this paper, the authors follow the transformational approach. In contrast to previous approaches in the literature, they impose no restrictions on the logic programs to be analyzed. In addition, the analysis of the transformed term rewriting systems can easily be automated using existing techniques and tools, such as the system AProVE [1], one of the most successful termination provers for term rewriting systems.

A key idea in this paper is the discovery that variables in a logic programming language can be seen as infinite terms in the term rewriting framework. This idea is then combined with the use of argument filtering to get rid of these infinite terms, so that the analysis essentially boils down to an ordinary termination analysis for term rewriting systems over finite terms.

In conclusion, this is a must-read paper for anyone who is interested in the termination analysis of logic programming languages.