Term Rewriting

Term rewriting is an important computational model with applications in algebra, software engineering, declarative programming, and theorem proving. In term rewriting, computation is achieved by directed equations and pattern matching. In this tutorial we give an introduction to term rewriting. The tutorial is organized as follows. After presenting several motivating examples, we explain the basic concepts and results in term rewriting: abstract rewriting, equational reasoning, termination techniques, confluence criteria, completion, strategies, and modularity. The tutorial concludes with a selection of more specialized topics as well as more recent developments in term rewriting: narrowing, advanced termination techniques (dependency pairs), conditional rewriting, rewriting modulo, tree automata techniques, and higher-order rewriting.