Term Rewriting Systems (WS21/22) [beendet]

Lecture: Prof. Franz Baader

Tutorials: Dr.-Ing. Stefan Borgwardt

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 will be held online, but synchronous using a video conferencing tool. Videos recorded during the lecture will be made available afterward. It takes place twice a week (Tuesdays and Thursdays 16:40–18:10) and is accompanied by weekly tutorials (Wednesdays 14:50–16:20 in room APB/E005). 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 video conference and other material will be provided for registered participants within OPAL.

The organizational details will be discussed in the first lecture, which starts on Tuesday, October 12, at 16:40. The first tutorial will take place on Wednesday, October 20, at 14:50 in room APB/E005.

SWS/Modules

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 Computational Logic: MCL-TCSL (Theoretical Computer Science and Logic), MCL-PI (Principles of Inference), MCL-AI (Artificial Intelligence)
• Master Computational Modeling and Simulation: CMS-LM-ADV (Logical Modeling: ), CMS-LM-MOC (Logical Modeling: Models of Computation)

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