Skip to Main content Skip to Navigation
Reports

Termination Proofs Using gpo Ordering Constraints : Extended Version

Thomas Genet 1 Isabelle Gnaedig 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We present here an algorithm for proving termination of term rewriting systems by \gpo ordering constraint solving. The algorithm gives, as automatically as possible, an appropriate instance of the gpo generic ordering proving termination of a given system. Constraint solving is done efficiently thanks to a DAG shared term data structure.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00073604
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 1:17:54 PM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM
Long-term archiving on: : Sunday, April 4, 2010 - 11:51:43 PM

Identifiers

  • HAL Id : inria-00073604, version 1

Collections

Citation

Thomas Genet, Isabelle Gnaedig. Termination Proofs Using gpo Ordering Constraints : Extended Version. [Research Report] RR-3087, INRIA. 1997, pp.37. ⟨inria-00073604⟩

Share

Metrics

Record views

238

Files downloads

157