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 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 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: 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 lecture on unification.

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