Syllabus
 
Rewriting in Computer Science and Logic (326.007)
Franz Winkler
 
Time: Tue 16.15 - 17.45     Place: T 112     Starting date: March 9, 2004

This lecture is intended to give an introduction to term rewriting systems and their application in computer science and logic. In particular we will discuss general reduction relations, properties of reduction systems such as confluence and termination, completion procedures (Knuth-Bendix procedure) for word rewriting systems and term rewriting systems.

The theory of rewriting is fundamental to concepts in constructive algebra, such as Gröbner bases, and also to concepts in logic, such as decision of equational theories (e.g. the theory of groups).

References

J. Avenhaus, Reduktionssysteme, Springer-Verlag, 1995

F. Baader, T. Nipkow, Term Rewriting and All That, Cambridge Univ. Press, 1998

R.V. Book, F. Otto, String-Rewriting Systems, Springer-Verlag, 1993