Polynomial interpretations as a basis for termination analysis of logic programs

This paper introduces a new technique for termination analysis of definite logic programs (LPs) based on polynomial interpretations. The principle of this technique is to map each function and predicate symbol to a polynomial over some subset of natural numbers, like it has been done in proving termination of term rewriting systems. Such polynomial interpretations can be seen as a direct generalisation of the traditional techniques in termination analysis of LPs, where (semi-)linear norms and level mappings are used. Our extension generalises 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 polynomial interpretations that satisfy the termination conditions. Based on this approach, we implement a new tool, called Polytool, for automatic termination analysis of logic programs