Proving Existential Termination of Normal Logic Programs

The most important open problem in the study of termination for logic programs is that of existential termination. In this paper we present a powerful transformational methodology that provides necessary (and, under some conditions, sufficient) criteria for existential termination. The followed approach is to develop a suitable transformation from logic programs to Term Rewriting Systems (TRSs), such that proving termination of the obtained TRS implies existential termination of the original logic program. Thus, all the extensive amount of work on termination for TRSs can be automatically used in the logic programming setting. Moreover, the approach is also able to cope with the dual notion of universal termination: in fact, a whole spectrum of termination properties, said k-termination, is investigated, of which universal and existential termination are the extremes. Also, a satisfactory treatment to the problem of termination for logic programming with negation is achieved. This way we provide a unique, uniform approach covering all these different notions of termination.