Multiset Path Orderings and Their Application to Termination of Term Rewriting Systems

Abstract

In this expository paper, a comprehensive study of multiset orderings, nested multiset orderings and multiset path orderings is presented. In particular, it is illustrated how multiset path orderings admit the use of relatively simple and intuitive termination functions that lead to termination of  a class of term rewriting systems.