Termination Proofs Using gpo Ordering Constraints : Extended Version
Thomas Genet, Isabelle Gnaedig, 54 - Villers-les-Nancy (France). Unite de Recherche de Lorraine Institut National de Recherche en Informatique et en Automatique (INRIA) · OpenGrey (Institut de l'Information Scientifique et Technique) · 1997
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.