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
Dr. rer. nat. Rafael Peñaloza
Course Description
Organisation
The lecture takes place twice a week. Additionally, there is a
weekly exercise session held by
Marcel Lippmann.
Exercise sheets will be available approximately one week before the
session.
The lectures and the exercise sessions 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 exercise sessions can be found in the table below.
Announcements:
The lectures and the exercise sessions 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 exercise sessions can be found in the table below.
Announcements:
- The exercise sessions will start on 16 April.
- The lecture will start on 8 April.
Tuesday | Wednesday | Thursday | |
7 April to 11 April | Lecture | Lecture | Lecture |
14 April to 18 April | Lecture | Exercise session (exercise sheet 1) |
Lecture |
21 April to 25 April | Lecture | Exercise session (exercise sheet 2) |
Lecture |
28 April to 2 May | Lecture | Exercise session (exercise sheet 3) |
May Day |
5 May to 9 May | Lecture | Exercise session (exercise sheet 4) |
Lecture |
12 May to 16 May | Lecture | Exercise session (exercise sheet 5) |
Lecture |
19 May to 23 May | Lecture | Dies academicus | Lecture |
26 May to 30 May | — | Exercise session (exercise sheet 6) |
Ascension Day |
2 June to 6 June | Lecture | Lecture | Lecture |
9 June to 13 June | Pentecost | Pentecost | Pentecost |
16 June to 20 June | Lecture | Exercise session (exercise sheet 7) |
Lecture |
23 June to 27 June | Lecture | Exercise session (exercise sheet 8) |
Lecture |
30 June to 4 July | Lecture | Exercise session (exercise sheet 9) |
Output |
7 July to 11 July | Lecture | Exercise session (exercise sheet 10) |
Lecture |
14 July to 18 July | Lecture | Exercise session (exercise sheet 11) |
— |
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 introductory session:
We provide, however, the slides for the introductory session:
- Chapter 1 (corrected)
Literature
The lecture is based on:
Franz Baader and Tobias Nipkow:
Term Rewriting and All That.
Cambridge University Press, 1998.