Title: Polytool: Polynomial interpretations as a basis for termination analysis of logic programs
Authors: Nguyen, Manh Thang
De Schreye, Danny ×
Giesl, Juergen
Schneider-Kamp, Peter #
Issue Date: 11-Jan-2011
Publisher: Cambridge University Press
Series Title: Theory and Practice of Logic Programming vol:11 pages:33-63
Abstract: Our goal is to study the feasibility of porting termination analysis techniques developed
for one programming paradigm to another paradigm. In this paper, we 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) ter-
mination 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. Our extension general-
izes these to arbitrary polynomials. We extend a number of standard concepts and results
on termination analysis to the context of polynomial interpretations. We also propose a
constraint-based approach for automatically generating polynomial interpretations that
satisfy the termination conditions. Based on this approach, we implemented a new tool,
called Polytool, for automatic termination analysis of LPs.
ISSN: 1471-0684
Publication status: published
KU Leuven publication type: IT
Appears in Collections:Informatics Section
× corresponding author
# (joint) last author

Files in This Item:
File Description Status SizeFormat
TPLPsubmission_sent.pdf Published 332KbAdobe PDFView/Open


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

© Web of science