Skip to Main content Skip to Navigation
Reports

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.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00075384
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 6:06:40 PM
Last modification on : Thursday, February 11, 2021 - 2:48:31 PM
Long-term archiving on: : Tuesday, April 12, 2011 - 10:51:20 PM

Identifiers

  • HAL Id : inria-00075384, version 1

Collections

Citation

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

Share

Metrics

Record views

100

Files downloads

71