Inferring Termination Conditions for Logic Programs using Backwards Analysis

Samir Genaim and Michael Codish   

Proceedings of the Eighth International Conference on Logic for Programming, Artificial Intelligence and Reasoning; 2001


This paper focuses on the inference of modes for which a logic program is guaranteed to terminate. This generalizes traditional termination analysis where an analyzer tries to verify termination for a specified mode. The contribution is a methodology which combines traditional termination analysis and backwards analysis to obtain termination inference. This leads to a better understanding of termination inference, simplifies its formal justification, and facilitates implementation. We evaluate the application of this approach to enhance an existing termination analyzer to perform also termination inference.

Available:    bibtex entry   postscript

Related sites:   technical report version   An online implementation   A paper on Termination Analysis

Michael Codish
The Department of Computer Science
Ben-Gurion University of the Negev
PoB 653, Beer-Sheva, 84105, Israel

© copyright notice