Title: Proving termination by invariance relations
Authors: Pilozzi, Paolo ×
De Schreye, Danny #
Issue Date: Jul-2009
Publisher: Springer
Series Title: Lecture Notes in Computer Science vol:5649 pages:499-503
Conference: International Conference on Logic Programming edition:25 location:Pasadena, California, U.S.A. date:14-17 July 2009
Abstract: We propose a new constraint-based approach to termination analysis, applicable to Logic Programming (LP) and Constraint Handling Rules (CHR). Our approach further extends the existing constraint-based approaches for LP based on polynomial interpretations and introduces a whole new level of expressivity. We can handle problems such as bounded increase and integer arithmetic, elegantly. Furthermore, we are able to prove termination of programs that only terminate for subsets of the considered queries. Examples are algorithms that manipulate graphs and that only terminate if the graph in the input is cycle-free. This information cannot be represented, using the existing techniques in termination analysis. Therefore, we introduce invariance relations, representing relations among terms that hold on atoms during calls to the program. These relations can also be derived in a constraint-based manner and they can be used as a basis for a more expressive interpretation of the atoms of the program. We discuss our technique in the context of CHR, solving an important class of open problems containing transitivity rules. We also demonstrate the technique in an LP context and show that it is more powerful than existing constraint-based approaches.
ISSN: 0302-9743
Publication status: published
KU Leuven publication type: IC
Appears in Collections:Informatics Section
× corresponding author
# (joint) last author

Files in This Item:
File Description Status SizeFormat
ICLPCamRedPTIR.pdfMain article Published 118KbAdobe PDFView/Open


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

© Web of science