Termination

This chapter gives an overview of techniques for proving termination of firstorder term rewriting systems. Three kinds of techniques arc distinguished: semanticsl methods, syntactical methods and transformational methods. Semantical methods are based on finding a suitable interpretation. They are suitable for all terminating systems but are hard to automate. Syntactical methods like the recursive path order can be automated in a straightforward manner but only apply for a restricted class of term rewriting systems. Therefore a number of transformational methods has been developed by which term rewriting systems outside this class can be transformed to systems inside this class in such a way that termination of the original systems can be concluded