Seminar: Advanced Topics in Term Rewriting

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 seminar is about advanced topics that have not been captured in the lecture Term Rewriting Systems held in the summer semester 2014.

Prerequisites: Knowing the basic material from the lecture Term Rewriting Systems would be helpful.


There is an initial meeting on 24 October 2014 at 14.50 in room INF/3027. There, topics are assigned to interested students and further organisational matters are covered.

The students taking the seminar should get acquainted with their respective topic, write a report (c. 15 pages) about it, and give a presentation (of 25 minutes) at the end of the semester. They receive indiviual supervision by Prof. Dr.-Ing. Franz Baader and Dr. Marcel Lippmann.

The topics have been assigned as follows:

Student Topic Supervisor
Kilian Gebhardt Gröbner Bases and Buchberger's Algorithm Dr. Lippmann
Maximilian Pensel Combining Word Problems Prof. Baader
Andrea Condoluci Equational Unification: Associative and Commutative Functions Dr. Lippmann
Florian Starke Equational Unification: Boolean Rings Prof. Baader

The students are expected to stick to the following schedule.


SWS: –/2/–

This course can be used in the following modules:


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