
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 lefthand side can be replaced by the righthand side, but not
vice versa. This constitutes a Turingcomplete 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 KnuthBendix completion can (sometimes) be used
to make nonconfluent, but terminating term rewriting systems confluent.

© ESSLLI 2005 Organising Committee 
20050124  