Unifying Semantic Path Order and Weighted Path Order

Teppei Saito, Nao Hirokawa

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 unifica…