## Term Rewriting Systems |
Technische Universität Dresden |

Term rewriting systems can be used to compute in structures that are defined by equations. They are thus an important tool in automated deduction, algebraic specification, and functional programming. The course introduces important properties such as termination and confluence in the framework of abstract reduction systems, gives a brief introduction into universal algebra, and then concentrates on confluence, termination, and completion of term rewriting systems.

Prerequisites: Basic notions from a course on discrete algebraic structures would be helpful.

The lecture takes place twice a week in room GRU 350: Tuesday 16:40-18:10 and Thursday 14:50-16:20 (observe: time for Thursday has changed).

The exercise group takes place on Wednesday 11:20-12:40 also in room GRU 350 and is held by Ulrike Sattler.

There is an extra exercise group on friday, May 23, 2003 in DS5 (14:50 - 16:20) in room 350 to compensate for the exercises we missed due to the academic day on May 7.

The exercises can be downloaded in Postscript format (the exercises for next week will be available on friday at noon this week, possibly earlier):

- 1. Exercise sheet
- 2. Exercise sheet
- 3. Exercise sheet
- 4. Exercise sheet
- 5. Exercise sheet
- 6. Exercise sheet
- 7. Exercise sheet
- 8. Exercise sheet
- 9. Exercise sheet
- 10. Exercise sheet
- 11. Exercise sheet
- 12. Exercise sheet
- 13. Exercise sheet
- 14. Exercise sheet

- present at least four exercises in front of the exercise group;

- pass an oral examination at the end of the term performed by Prof. Baader.

- F. Baader, T. Nipkow.
*Term Rewriting and All That.*ISBN 0-521-77920-0, Cambridge University Press, 1998

Ulrike Sattler