For Logic Programming (LP), termination analysis is done by mapping terms and atoms to a well-founded set of natural numbers by means of norms and level mappings. Proving termination is based on the search for a suitable norm and level mapping such that the mapped value of the initial predicate call is bounded and of the running predicate calls decrease under the mapping. Automated termination proof, however, does not take into account all computational states. It focuses on verifying the decrease in size of recursive predicate calls, which correspond to the loops that the execution passes through. Most termination techniques in LP are. A restriction of semilinear norms is that a lot of examples require more powerful norms to verify their termination.
We developed a general framework based on the use of polynomial interpretations as a basis for termination proof of LP in [1]. This approach can be seen as a direct generalisation of currently used techniques in LP termination based on semilinear norms and linear level mappings, where linear polynomial functions are extended to arbitrary polynomials. The use of polynomial interpretation for proving termination was first introduced by [2] and is now one of the best known and widely used approaches in Term Rewriting Systems (TRS).
We implemented an automated tool (Polytool) for termination analysis based on this approach [3]. It is embedded within the constraint-based approach developed in [4] and combined with the type inference engine of Janssens and Broynooghe [5] and the nonlinear Diophantine constraint solver (AProVE-SAT) developed by Carsten Fuhs, J{\"u}rgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, Ren{\'e} Thiemann and Harald Zankl [6] to provide a completely automated system.