Abstract

It is well-known that termination of finite term of rewriting systems is generally undecidable. NoItwithstanding, a remarkable result is that, rewriting systems are Turing complete. A number of methods have been developed to establish termination for certain term of rewriting systems, particularly occurring in practical situations. In this paper, we present an overview of the existing methods used for termination proofs. We also outline areas of applications of term rewriting systems along with recent developments in regard to automated termination proofs.

Key words: Confluence, rewriting, term, termination, turing complete.