Term rewriting systems: a tutorial
Jan Willem Klop · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1987
Term Rewriting Systems play an important role in various areas, such as abstract data type specifications, implementations of functional languages and automated deduction.In this tutorial we introduce some of the basic concepts and facts for TRSs.No attempt is made to present a comprehensive survey: e.g. the tutorial does not contain material about conditional TRSs or equational TRSs.The spirit of the material presented here is syntactic rather than semantic.An emphasis is put on Abstract Reduction Systems, of which not only TRSs are instances, but also Semi-Thue Systems, tree replacement systems, graph rewrite systems.As an example of an important termination proof technique we present the recursive path orderings in a new presentation.