Termination by completion

Abstract : This paper presents a completion procedure for proving termination of term rewrite systems. It works as follows. Given a term rewrite system R supposed to terminate and a term rewrite system T used to transform R, the completion builds an auxiliary term rewrite system S, the system transformed of R by T. The termination of S and T associated with a property called local cooperation implies the termination of R. If the process terminates this provides a mechanical proof of the termination of R.
Type de document :
Rapport
[Research Report] RR-1174, INRIA. 1990
Liste complète des métadonnées

https://hal.inria.fr/inria-00075384
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 18:06:40
Dernière modification le : samedi 17 septembre 2016 - 01:06:51
Document(s) archivé(s) le : mardi 12 avril 2011 - 22:51:20

Fichiers

Identifiants

  • HAL Id : inria-00075384, version 1

Collections

Citation

François Bellegarde, Pierre Lescanne. Termination by completion. [Research Report] RR-1174, INRIA. 1990. 〈inria-00075384〉

Partager

Métriques

Consultations de la notice

79

Téléchargements de fichiers

46