Termination by completion - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 1990

Termination by completion

François Bellegarde
  • Fonction : Auteur
Pierre Lescanne
  • Fonction : Auteur

Résumé

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.

Domaines

Autre [cs.OH]
Fichier principal
Vignette du fichier
RR-1174.pdf (1.07 Mo) Télécharger le fichier

Dates et versions

inria-00075384 , version 1 (24-05-2006)

Identifiants

  • HAL Id : inria-00075384 , version 1

Citer

François Bellegarde, Pierre Lescanne. Termination by completion. [Research Report] RR-1174, INRIA. 1990. ⟨inria-00075384⟩
44 Consultations
32 Téléchargements

Partager

Gmail Facebook X LinkedIn More