Inferring termination conditions for logic programs using backwards analysis

Abstract

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.