Proving termination by invariance relations

Abstract. We propose a new constraint-based approach to termination analysis, applicable to Logic Programming (LP) and Constraint Han-dling Rules (CHR). Our approach further extends the existing constraint-based approaches for LP based on polynomial interpretations and intro-duces 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 sub-sets 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, rep-resenting relations among terms that hold on atoms during calls to the program. These relations can also be derived in a constraint-based man-ner 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 o