8481 articles  [english version]

inria-00073604, version 1

Termination Proofs Using gpo Ordering Constraints : Extended Version

Thomas Genet 1, Isabelle Gnaedig () 1

N° RR-3087 (1997)

Résumé : 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.

  • 1 :  PROTHEO (INRIA Lorraine - LORIA)
  • INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
  • Domaine : Informatique/Autre
  • Mots-clés : term rewriting – termination proof – ordering constraint solving
  • Référence interne : RR-3087
 
  • inria-00073604, version 1
  • http://hal.inria.fr/inria-00073604
  • oai:hal.inria.fr:inria-00073604
  • Contributeur : Rapport De Recherche Inria <>
  • Soumis le : Mercredi 24 Mai 2006, 13:17:54
  • Dernière modification le : Mercredi 21 Juin 2006, 09:46:32