Polytool: Proving Termination Automatically
based on Polynomial Interpretations

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.

For Downloaders

  • Download the source code of Polytool
  • Download examples (Termination Problems Database) for termination verification
  • An online version of the Polytool: Under development
  • References

  • Nguyen, M. T. and De Schreye, D., Polynomial Interpretations as a Basis for Termination Analysis of Logic Programs (full paper), the Twenty First International Conference on Logic Programming, pp. 311-326, LNCS 3668, Maurizio Gabbrielli and Gopal Gupta Eds., Barcelona, Spain, October 2005 (download *.ps)
  • Nguyen, M. T. and De Schreye, D., Giesl, J., and Schneider-Kamp, P., Polytool: Proving Termination Automatically based on Polynomial Interpretations, Technical Report, Department of Computer Science, K.U.Leuven, Belgium. (download *.pdf)
  • Other Termination Analyzers

  • Hasta-La-Vista
  • TerminWeb
  • cTi-nTi
  • TALP
  • AProVE