An Improved General Path Order

摘要

We define a strong and versatile termination order for term rewriting systems, called the Improved General Path Order, which simplifies and strengthens Dershowitz/Hoot’s General Path Order. We demonstrate the power of the Improved General Path Order by proofs of termination of non-trivial examples, among them a medium-scale term rewriting system that models a lift control.