Polytool: Polynomial interpretations as a basis for termination analysis of logic programs

This paper reports on work that was done in a project called "Termination analysis: crossing paradigm borders". The aim of the project is to study the feasibility of porting termination analysis techniques developed for one programming paradigm to another paradigm. In this paper, we report on part of the results of this project, namely, the study of porting termination analysis techniques based on polynomial interpretation - very well known in the context of term rewrite systems (TRS) - to obtain new (non-transformational) termination analysis techniques for definite logic programs (LP). We show how this leads to an approach that can be seen as a direct generalization of the traditional techniques in termination analysis of LP, where linear norms and level mappings are used. Our extension generalizes these to arbitrary polynomials. We extend a number of standard concepts and results on termination analysis to the context of polynomial interpretations. We propose a constraint based approach for automatically generating poly- nomial interpretations that satisfy the termination conditions. Based on this approach, we implement a new tool, called Polytool, for automatic termination analysis of logic programs.nrpages: 35status: publishe