Term Rewriting Systems

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. 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 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: 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

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:

• Chapter 1 (corrected)

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