Termination Analysis of Logic Programs based on Dependency Graphs

Abstract. This paper introduces a modular framework for termination analysis of logic programming. To this end, we adapt the notions of de-pendency pairs and dependency graphs (which were developed for term rewriting) to the logic programming domain. The main idea of the ap-proach is that termination conditions for a program are established based on the decomposition of its dependency graph into its strongly connected components. These conditions can then be analysed separately by pos-sibly dierent well-founded orders. We propose a constraint-based ap-proach for automating the framework. Then, for example, termination techniques based on polynomial interpretations can be plugged in as a component to generate well-founded orders.