Mechanically proving termination using polynomial interpretations

• Tipo: Artigo em Revista Científica Internacional
• Data: 2005

Autores

Evelyne Contejean (Autor) Outra; Claude Marche (Autor) Outra; Ana Paula Tomas (Autor) FCUP; Xavier Urbain (Autor) Outra

Revista

Título: Journal of Automated Reasoning

Vol. 34

Páginas: 325-363

ISSN: 0168-7433

Editora: Springer Nature

Indexação

ISI Web of Knowledge - 38 Citações

Scopus - 51 Citações

Classificação Científica

FOS: Ciências exactas e naturais > Ciências da computação e da informação

Outras Informações

ID Authenticus: 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.

Idioma: Inglês

Tipo (Avaliação Docente): Científica

Nº de páginas: 39