Polytool: Polynomial Interpretations as a Basis for Termination Analysis of Logic Programs

Download Now Date Added: Dec 2009
Format: PDF

The authors' goal is to study the feasibility of porting termination analysis techniques developed for one programming paradigm to another paradigm. In this paper, they show how to adapt termination analysis techniques based on polynomial interpretations - very well known in the context of Term Rewrite Systems (TRSs) - to obtain new (non-transformational) termination analysis techniques for definite Logic Programs (LPs). This leads to an approach that can be seen as a direct generalization of the traditional techniques in termination analysis of LPs, where linear norms and level mappings are used. Their extension generalizes these to arbitrary polynomials. They extend a number of standard concepts and results on termination analysis to the context of polynomial interpretations.