Inferring Termination Conditions for Logic Programs Using Backwards Analysis

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.

• Type: Conference
• Year: 2001
• Where: LPAR
• Authors: Samir Genaim, Michael Codish
• Keywords: Automated Reasoning, LPAR 2001, Termination Analyzer, Termination Inference, Traditional Termination Analysis