MOVES Seminar, 16 Aug 2007, 14:00

Termination Analysis of Logic Programs based on Dependency Graphs

 

Peter Schneider-Kamp

 

 

Abstract:

This paper introduces a modular framework for terminationanalysis of logic programming. To this end, we adapt the notions of dependencypairs and dependency graphs (which were developed for termrewriting) to the logic programming domain. The main idea of the approachis that termination conditions for a program are established basedon the decomposition of its dependency graph into its strongly connectedcomponents. These conditions can then be analysed separately by possiblydifferent well-founded orders. We propose a constraint-based approachfor automating the framework. Then, for example, terminationtechniques based on polynomial interpretations can be plugged in as acomponent to generate well-founded orders.