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.
Type de document :
Rapport
[Research Report] RR-3087, INRIA. 1997, pp.37
Liste complète des métadonnées

https://hal.inria.fr/inria-00073604
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 13:17:54
Dernière modification le : lundi 17 septembre 2018 - 13:42:01
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:51:43

Fichiers

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

213

Téléchargements de fichiers

117