Termination of Order-Sorted Rewriting with Non-minimal Signatures

摘要

In this paper, we extend the Gnaedig's re- sults[2],[3] on termination of order-sorted rewriting. Gnaedig required a condition for order-sorted signatures, called minimal- ity, for the termination proof. We get rid of this restriction by introducing a transformation from a TRS with an arbitrary order- sorted signature to another TRS with a minimal signature, and proving that this transformation preserves termination.