Check your Ordering : Termination Proofs and Open Problems

Abstract

Termination is a decisive property of term rewriting systems that is often needed. Simplification orderings provide a mechanism for proving this property. The power of such an ordering depends on the number of examples (occurring in practice) to which it can successfully be applied. In addition to a brief introduction to the presented simplification orderings, this report contains a large collection of term rewriting systems all of which were tested for completion by our completion environment COMTES. In a lot of cases simplification orderings can be found that enable the generation of canonical systems. However, a lot of examples exist for which the problem of completion cannot be solved.