Term Rewriting Systems
Lecturer: Prof. Dr.-Ing. Franz Baader
Tutorials: Dipl.-Math. Francesco Kriegel
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.
Organisation
The lecture will take place in room APB/E005 twice a week on Tuesdays and Thursdays, and is accompanied by weekly tutorials in room APB/E005 on Wednesdays. Exercise sheets will be available approximately one week in advance. The exact distribution of lectures and tutorials can be found in the table below.
Schedule
| Tuesday 16:40–18:10 |
Wednesday 14:50–16:20 |
Thursday 16:40–18:10 |
|
|---|---|---|---|
| 10 April — 12 April |
Lecture | Tutorial (Exercise Sheet 1) |
Lecture |
| 17 April — 19 April |
Lecture | Tutorial (Exercise Sheet 2) |
Lecture |
| 24 April — 26 April |
Lecture | Tutorial (Exercise Sheet 3) |
Lecture |
| 1 May — 3 May |
(1st May) | Tutorial (Exercise Sheet 4) |
Lecture |
| 8 May — 10 May |
Tutorial (Exercise Sheet 5) |
Lecture | (Ascension Day) |
| 15 May — 17 May |
Lecture | Tutorial (Exercise Sheet 6) |
Lecture |
| 22 May — 24 May |
(Pentecost) | (Pentecost) | (Pentecost) |
| 29 May — 31 May |
Lecture | Tutorial (Exercise Sheet 7) |
Lecture |
| 5 June — 7 June |
Tutorial (Exercise Sheet 8) |
(Dies academicus) | Lecture |
| 12 June — 14 June |
Lecture | Tutorial (Exercise Sheet 9) |
Lecture |
| 19 June — 21 June |
Lecture | Tutorial (Exercise Sheet 10) |
Lecture |
| 26 June — 28 June |
Lecture | Tutorial (Exercise Sheet 11) |
Lecture |
| 3 July — 5 July |
Lecture | Tutorial (Exercise Sheet 12) |
Lecture |
| 10 July — 12 July |
Lecture | Tutorial (Exercise Sheet 13) |
Lecture |
| 17 July — 19 July |
Lecture | Tutorial (Q&A Session) |
Lecture |
SWS/Modules
SWS: 4/2/–
This course can be used in the following
modules:
- Bachelor-Studiengang Informatik: INF-B-510 (Vertiefung), INF-B-520 (Vertiefung zur Bachelor-Arbeit)
- Master-Studiengang Informatik: INF-BAS6 (Theoretische Informatik), INF-VERT6 (Theoretische Informatik)
- Master in Computational Logic: MCL-TCSL (Theoretical Computer Science and Logic), MCL-PI (Principles of Inference)
- Diplom-Studiengang Informatik (Studienordnung 2004): Fachgebiet Theorie der Programmierung, Fachgebiet Intelligente Systeme
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 introductory lecture and for the lecture on unification.
Literature
The lecture is based on: Franz Baader and Tobias Nipkow: Term Rewriting and All That. Cambridge University Press, 1998.