Description

Term rewriting is a branch of theoretical computer science which 
combines elements of logic, universal algebra, automated theorem 
proving and functional programming. Its foundation is equational 
logic.  What distinguishes term rewriting from equational logic 
is that equations are used as directed replacement rules, i.e., 
the left-hand side can be replaced by the right-hand side, but not 
vice versa. This constitutes a Turing-complete computational model 
which is very close to functional programming. It has many applications 
in mathematics and computer science since it applies in any context 
where efficient methods for reasoning with equations are required. The
important properties of term rewriting systems that make this efficient
reasoning possible are termination and confluence. 

After a short motivation of their usefulness, the course introduces
and analyzes these important properties, describes methods for proving
them, and shows how Knuth-Bendix completion can (sometimes) be used 
to make non-confluent, but terminating term rewriting systems confluent.