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 in room E05: Tuesdays 16:40–18:10 and Thursdays 16:40–18:10.

Announcements:

• On 2nd February, there will be no lecture.
• On 26th January, there will be no lecture.
• On 12th January, there will be no lecture.
• A typo in exercise 56 (definition of E₁) has been corrected on exercise sheet 11.
• On 13th December (16:40–18:10), there will be an exercise session instead of a lecture. The lecture of this day is shifted to 14th December (14:50–16:20).
• The 16th November is a public holiday (Day of Prayer and Repentance). The exercise session of this day is shifted to 18th November (14:50–16:20).
• On 2nd November, there will be a lecture instead of an exercise session. In return, there will be an exercise session instead of a lecture on 3rd November.
• The exercise sessions will start on 26th October.
• On 19th October (14:50–16:20), there will be a lecture instead of an exercise session.
• The lecture will start on 18th October.

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

• Chapter 1
• Buchberger's Algorithm

A weekly exercise session will be held by Marcel Lippmann on Wednesdays 14:50–16:20 in room E05.

Exercise sheets will be available here approximately one week before the session.

• Exercise Sheet 1 (26th October)
• Exercise Sheet 2 (3rd November)
• Exercise Sheet 3 (9th November)
• Exercise Sheet 4 (18th November)
• Exercise Sheet 5 (23rd November)
• Exercise Sheet 6 (30th November)
• Exercise Sheet 7 (7th December)
• Exercise Sheet 8 (13th December)
• Exercise Sheet 9 (21st December)
• Exercise Sheet 10 (4th January)
• Exercise Sheet 11 (11th January)
• Exercise Sheet 12 (18th January)
• Exercise Sheet 13 (25th January)
• Exercise Sheet 14 (1st February)

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