The termination problem of programs is in general an undecidable problem. However, in the context of some programming paradigms, there has been a lot of research in finding useful decidable criteria characterizing certain subclasses of programs that guarantee termination. This paper presents new criteria guaranteeing termination of logic programs with function symbols.

The introduction motivates the criteria later developed by presenting an example of a logic program with function symbols that is easily recognized to be terminating, but is not covered by existing criteria. This motivating example is followed by a survey of the existing work and existing algorithms for termination detection in the area of logic programs. The following two sections briefly recapitulate the syntax and semantics of logic programs and some classes of terminating logic programs recently researched.

The main part of the paper introduces the class of mapping-restricted programs, which extends the class of argument-restricted programs by, in a way, abstracting the argument position to mappings from the argument position to strings of function symbols and then presenting a criterion on these structures. It is then shown that a program matching this criterion is terminating, that the class of mapping-restricted programs is a strict superset of the class of argument-restricted programs, and that this class is incomparable with two other classes of terminating programs. For the algorithms to be described and investigated, the program is transformed first into a unitary program that contains only unitary function symbols and has the same behavior with respect to the criterion defined. This unitary program is then checked, and if the check succeeds, it is shown that the original program also satisfies the criterion. The following chapter investigates the decidability of the criterion and the complexity of the decision procedure. The main result is that the complexity of the checking is EXPTIME-complete.

The following section begins with an example illustrating that the method fails to prove the termination of some programs easily seen to be terminating because the method for constructing unitary programs obscures information about arguments existing in the original programs. This leads to two improved algorithms for constructing the unitary program; again, relevant properties of these approaches are proven, essentially maintaining the previous complexity result. The paper ends with a short conclusion.

The paper is very readable, containing very nice motivating examples and enough details to follow every argument. Some of the proofs rely on known complexity results, linear temporal logics, and computation tree logic, and in the appendix the reader can find the basics of these two logics as well as references to the complexity results. Some examples and more detailed algorithms have also been relegated to the appendix, so all details are available for the interested reader. It was a very good paper to read and only left me wondering whether the authors also consulted the very rich work on termination of term rewriting systems and whether there is some overlap there. I had the nagging feeling that there might be some synergy from looking into this field and comparing approaches.