Persistence of Termination for Term Rewriting Systems with Ordered Sorts

M. Iwami (Japan)


: Model-based reasoning, term rewriting sys tem, termination, persistence


A property P is persistent if for any many-sorted term rewriting system R, R has the property P if and only if term rewriting system (R), which results from R by omitting its sort information, has the property P. Zantema showed that termination is persistent for term rewriting systems without collapsing or duplicating rules. In this paper, we show that the Zantema's result can be extended to term rewriting systems on ordered sorts, i.e., termina tion is persistent for term rewriting systems on ordered sorts without collapsing, decreasing or duplicating rules. Furthermore we give the example as application of this result. Also we obtain that completeness is persistent for this class of term rewriting systems.

Important Links:

Go Back