Rewriting: Completion and Strategies
Term rewriting is a powerful model of computation that underlies much of declarative programming and which is heavily used in symbolic computation in mathematics, theorem proving, and protocol verification.
In the first part we give an introduction to first-order term rewriting and the completion procedure. The latter yields, if successful, a method to solve the word problem.
In the second part we consider strategies: recipes telling us how to rewrite a term in order to obtain a rewrite sequence with a certain property.