Termination Proofs Using gpo Ordering Constraints : Extended Version
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.