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 16:40-18:10.
On 15.06, and 24.06 the lecture will take
place in Room GRU 370 and on 16.06 (11:15 - 12:45) in Room 470.
The exercise group will be held by Barbara Morawska. It meets on Wednesdays 11:10-12:40 in GRU 350.
The exercises can be downloaded in Postscript format (the
exercises for next week will be available on Friday at noon this week,
- exercises (for 7.04.04)
- exercises (for 14.04.04)
- exercises (for 21.04.04)
- exercises (for 28.04.04)
- exercises (for 5.05.04 -- Dies academicus! No meeting today.)
- exercises (for 12.05.04)
- exercises (for 19.05.04)
The additional meeting will be on 21.05.04 (Friday),
13:00 - 14:30, Room 351.
- exercises (for 26.05.04)
There will be tutorial on 27.05.04 (Thursday)
in the place of the lecture!
- exercises (for 27.05.04)
- exercises (
-- in Room: 470)
More changes! The next tutorial will take place on 22.06 (in Room 370, 16:40-18:10),
and there will be lecture on 16.06 (in Room 470, 11:15 - 12:45).
- exercises (for 23.06.04, Room 470)
There will be lecture in the place of the tutorial on 30.07, 11:15 - 12:45.
- exercises (for 1.07.04, 16:40-18:10)
- exercises (for 7.07.04) No lecture
on 6.07, and additional tutorial on 8.07 in place of the lecture!
- exercises (for 8.07.04, 16:40-18:10 )
- exercises (for 14.07.04),
solutions for the last exercises.
Credits / Examinations
Computational logic students can earn 9 credits by attending this lecture.
In order to get the credits, CL students have to meet both of the following two
Computer Science students are not obliged to present exercises, but are invited
to do so.
- 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.
The lecture is based on
- F. Baader, T. Nipkow. Term Rewriting and All That. ISBN 0-521-77920-0,
Cambridge University Press, 1998