Term Rewriting Systems

Prof. Dr.-Ing. Franz Baader

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.


The lecture takes place twice a week in room E05: Tuesdays 16:40–18:10 and Thursdays 16:40–18:10.



SWS: 4/2/–

This course can be used in the following modules:

Lecture Material


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.


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