Monotonic semantic path orders and weighted path orders are powerful reduction orders for proving termination of term rewrite systems. In this paper we present their simple unification as reduction orders and reduction pairs. We also discuss the use of it as ground total reduction orders.

翻译：单调语义路径序和加权路径序是用于证明项重写系统终止性的强大归约序。本文提出了它们作为归约序和归约对的简单统一形式，并进一步讨论了其作为基项全归约序的应用。