Term Rewriting Systems

Dr. rer. nat. Rafael Pe├▒aloza


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

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:

Literature

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