Term Rewriting Systems (WS24/25)

Lecture: Prof. Dr. Franz Baader

Tutorials: Dr. Francesco Kriegel

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.

Organization

The lecture takes place twice a week (Tuesdays and Thursdays 16:40–18:10 in room APB/E005) and is accompanied by weekly tutorials (Wednesdays 11:10–12:40 in room APB/E006). Exercise sheets will be made available approximately one week in advance of the respective tutorial.

To participate in the course, you need to register for the course in OPAL. Links for accessing the exercise sheets and other material will be provided for registered participants within OPAL.

The organisational details will be discussed in the first lecture, which starts on Tuesday, October 15, at 16:40  in room APB/E005. The first tutorial will take place on Wednesday, October 23, at 11:10 in room APB/E006.

SWS/Modules

SWS: 4/2/–
Modules: CMS‑LM‑ADV, CMS‑LM‑AI, CMS‑LM‑MOC, INF‑B‑510, INF‑B‑520, INF‑BAS2, INF‑BAS6, INF‑VERT2, INF‑VERT6, MCL‑AI, MCL‑PI, MCL‑TCSL

Literature

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

You can access the PDF of the book from within the network of TU Dresden (or via VPN) here:
https://www.cambridge.org/core/books/term-rewriting-and-all-that/71768055278D0DEF4FFC74722DE0D707