The aim of this survey is to present some of the basic concepts and facts about term rewriting systems (TRSs) which are obvious prerequisites for applications in various areas, such as abstract data type specifications, implementations of functional languages and automated deduction. The survey contains six sections.
In the first section many properties valid already for abstract rewriting systems are collected; this makes these properties also applicable to other rewrite systems, such as string rewrite systems, tree replacement systems etc. The second section discusses some basic issues in general TRSs.
In the third section a powerful termination proof technique based on Kruskal’s tree-embedding theorem is presented. Next, a short exposition of the Knuth-Bendix complection technique is given.The last part deals with regular TRSs and reduction strategies for such TRSs. The spirit of the material presented here is syntactic rather than semantic.