Constraint-based termination analysis of logic programs

Current norm-based automatic termination analysis techniques for logic prog rams can be split up into different components: inference of mode or type i nformation, derivation of models, generation of well-founded orders, and ve rification of the termination conditions themselves. Although providing hig h-precision results, these techniques suffer from an efficiency point of vi ew, as several of these analyses are often performed through abstract inter pretation. We present a new termination analysis which integrates the vario us components and produces a set of constraints that, when solvable, identi fies successful termination proofs. The proposed method is both efficient a nd precise. The use of constraint sets enables the propagation of informati on over all different phases while the need for multiple analyses is consid erably reduced.