Demand-driven and constraint-based automatic left-termination analysis for Logic Programs
Lee Naish · 1997
Current automatic termination analysis techniques can be split up into different components: inference of mode or type information, derivation of models, generation of well-founded orders and verification of the termination conditions themselves. Although providing high precision results, these techniques suffer from an efficiency point of view as several of these analyses are often performed through abstract interpretation. In this paper we first present a new termination analysis which integrates the various components and produces a set of constraints that, when solvable, identifies successful termination proofs. The proposed method is both efficient and precise. The use of constraint sets enables the propagation of information over all different phases while the need for multiple analyses is considerably reduced.