| Home > Publications > Reports > Informatics (CW) |
CW 412
Manh Thang Nguyen, and Danny De Schreye
Polynomial interpretations as a basis for termination analysis of logic programs
Abstract
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.
report.pdf (258K) / revised, August 2007.pdf (350K) / mailto: M.T. Nguyen