In this paper we present some original variations of the recursive
path ordering. Additionally we define a restricted semantic path
ordering which, in general, does not include the subterm relation,
but is shown to be monotonic. By combining both kind of
orderings we can prove (automatically) the termination of several
(non-simply terminating) examples.
CitationBorralleras, C., Rubio, A. "Path orderings, quasi-orderings and termination of term rewriting systems". 1997.
All rights reserved. This work is protected by the corresponding intellectual and industrial property rights. Without prejudice to any existing legal exemptions, reproduction, distribution, public communication or transformation of this work are prohibited without permission of the copyright holder. If you wish to make any use of the work not provided for in the law, please contact: firstname.lastname@example.org