Polytool: Proving Termination Automatically Based on Polynomial Interpretations

Abstract In this system description, we present Polytool, a fully automated system for proving left-termination of definite logic programs (LPs). The aim of Polytool is to extend the power of existing termination analysers by using well-founded orders based on polynomial interpretations. This is a direct extension of the well-founded orders based on (semi-)linear level mappings and norms that are used in most of the existing LP termination analysis systems.

Authors

• Manh Thang Nguyen
• Danny De Schreye

Keywords

No keywords are indexed for this paper.