Term Rewriting Systems

Technische Universität Dresden Institut für Theoretische Informatik Lehrstuhl für Automatentheorie

Prof. Dr.-Ing. Franz Baader

Course Description

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.

Organization

The lecture takes place twice a week in room E05: Tuesday 16:40-18:10 and Thursday 16:40-18:10.

Exercise Group

The exercise group will be held by Barbara Morawska. It meets on Wednesdays 14:50-16:20 in E05.

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. exercises (for Tuesday, 21.10.2008)
2. exercises (for Tuesday, 28.10.2008)
3. exercises (for Wednesday, 29.10.2008)
4. exercises (for Wednesday, 5.11.2008)
5. exercises (for Wednesday, 12.11.2008)
6. exercises (for Wednesday, 26.11.2008)
7. exercises (for Wednesday, 3.12.2008)
8. exercises (for Thursday, 11.12.2008)
9. exercises (for Wednesday, 17.12.2008)
10. exercises (for Thursday, 18.12.2008) ← additional tutorial!
11. exercises(7.01.2009)
12. exercises(14.01.2009)
13. exercises(for Wednesday, 21.01.2009)
14. exercises Tuesday, 03.02.2009 ← additional tutorial!
15. exercises(for Wednesday, 04.02.2009)

Credits / Examinations

1. present at least four exercises in front of the exercise group;
   
   
2. pass an oral examination at the end of the term performed by Prof. Baader.

Reference

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