Polynomial Interpretations as a Basis for Termination Analysis of Logic Programs

 

Manh Thang Nguyen

 

Abstract:

In this presentation, I introduces a technique for termination
analysis of denite logic programs based on polynomial
interpretations. The principle of this technique is to map each
function and predicate symbol to a polynomial over some domain 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 termination conditions. Based on this
approach, we implement a new tool, namely Polytool, for automatic
termination analysis of logic programs.