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.