Term Rewriting Systems

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.


The lecture will take place twice a week and is accompanied by weekly tutorials held by Dr. Marcel Lippmann. Exercise sheets will be available approximately one week in advance.

The lectures and the tutorials will take place in room E05 at the following times: Tuesdays 16.40–18.10, Wednesdays 14.50–16.20, and Thursdays 16.40–18.10. The exact distribution of lectures and tutorials can be found in the table below.

Tuesday Wednesday Thursday
4 April to 8 April Lecture Lecture
11 April to 15 April Lecture Tutorial
(Exercise Sheet 1)
18 April to 22 April Lecture Tutorial
(Exercise Sheet 2)
25 April to 29 April Lecture Tutorial
(Exercise Sheet 3)
2 May to 6 May Tutorial
(Exercise Sheet 4,
moved to Friday, 6 May, 13.00–14.30, APB/3027)
Lecture Ascension Day
9 May to 13 May Tutorial
(Exercise Sheet 5)
(moved to Friday, 13 May, 14.50–16.20, APB/3027)
16 May to 20 May Pentecost Pentecost Pentecost
23 May to 27 May Lecture Tutorial
(Exercise Sheet 6)
30 May to 3 June Lecture Dies academicus Tutorial
(Exercise Sheet 7)
6 June to 10 June Tutorial
(Exercise Sheet 8)
Lecture Lecture
(in APB/3027)
13 June to 17 June Lecture Lecture Tutorial
(Exercise Sheet 9)
20 June to 24 June Lecture Lecture
27 June to 1 July Tutorial
(Exercise Sheet 10/11)
Lecture Tutorial
(Exercise Sheet 10/11)
4 July to 8 July Lecture Tutorial
(Exercise Sheet 12)
11 July to 15 July Lecture Tutorial
(Exercise Sheet 13)


SWS: 4/2/–

This course can be used in the following modules:

Lecture Material

A script of this lecture is not available, and students are strongly recommended to copy what is written on the blackboard.

We provide, however, the slides for the lecture on unification.


The lecture is based on: Franz Baader and Tobias Nipkow: Term Rewriting and All That. Cambridge University Press, 1998.