Title: Polytool: Polynomial interpretations as a basis for termination analysis of logic programs
Authors: Nguyen, Manh Thang
De Schreye, Danny
Giesl, Jürgen
Schneider-Kamp, Peter
Issue Date: Jul-2009
Publisher: Department of Computer Science, K.U.Leuven
Series Title: CW Reports vol:CW558
Abstract: 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.
Publication status: published
KU Leuven publication type: IR
Appears in Collections:Informatics Section

Files in This Item:
File Description Status SizeFormat
CW558.pdfDocument Published 526KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.