Mechanically proving termination using polynomial interpretations

• Type: Article in International Scientific Journal
• Date: 2005

Authors

Evelyne Contejean (Author) Other; Claude Marche (Author) Other; Ana Paula Tomas (Author) FCUP; Xavier Urbain (Author) Other

Journal

Title: Journal of Automated Reasoning

Vol. 34

Pages: 325-363

ISSN: 0168-7433

Publisher: Springer Nature

Indexing

ISI Web of Knowledge - 38 Citations

Scopus - 51 Citations

Scientific classification

FOS: Natural sciences > Computer and information sciences

Other information

Authenticus ID: P-000-3MR

DOI: 10.1007/s10817-005-9022-x

Abstract (EN): For a long time, term orderings defined by polynomial interpretations were scarcely used in computer-aided termination proof of TRSs. But recently, the introduction of the dependency pairs approach achieved considerable progress w.r.t. automated termination proof, in particular by requiring from the underlying ordering much weaker properties than the classical approach. As a consequence, the noticeable power of a combination dependency pairs/polynomial orderings yielded a regain of interest for these interpretations. We describe criteria on polynomial interpretations for them to define weakly monotonic orderings. From these criteria, we obtain new techniques both for mechanically checking termination using a given polynomial interpretation and for finding such interpretations with full automation. With regard to automated search, we propose an original method for solving Diophantine constraints. We implemented these techniques into the CiME rewrite tool, and we provide some experimental results that show how useful polynomial orderings actually are in practice.

Language: English

Type (Professor's evaluation): Scientific

No. of pages: 39