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.
Chair of Automata Theory
Institute of Theoretical Computer Science
Faculty of Computer Science
Technische Universität Dresden
Institute of Theoretical Computer Science
Faculty of Computer Science
Technische Universität Dresden
Term Rewriting Systems
Prof. Dr.-Ing. Franz Baader
Course Description
Organisation
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.
Announcements:
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.
Announcements:
- The tutorials will start on 13 April.
- The lecture will start on 6 April.
Tuesday | Wednesday | Thursday | |
4 April to 8 April | Lecture | Lecture | |
11 April to 15 April | Lecture | Tutorial (Exercise Sheet 1) |
Lecture |
18 April to 22 April | Lecture | Tutorial (Exercise Sheet 2) |
Lecture |
25 April to 29 April | Lecture | Tutorial (Exercise Sheet 3) |
Lecture |
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) |
Lecture (moved to Friday, 13 May, 14.50–16.20, APB/3027) |
Lecture |
16 May to 20 May | Pentecost | Pentecost | Pentecost |
23 May to 27 May | Lecture | Tutorial (Exercise Sheet 6) |
Lecture |
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) |
Lecture |
11 July to 15 July | Lecture | Tutorial (Exercise Sheet 13) |
Lecture |
SWS/Modules
SWS: 4/2/–
This course can be used in the following modules:
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 lecture on unification.
We provide, however, the slides 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.