In this paper the Recursive Path Ordering is adapted for proving termination of rewriting incrementally. The new ordering, called Recursive Path Ordering with Modules, has as ingredients not only a precedence but also an underlying ordering ]_B. It can be used for incremental (innermost) termination proofs of hierarchical unions by defining ]_B as an extension of the termination proof obtained for the base system. Furthermore, there are practical situations in which such proofs can be done modularly.
展开▼
