Stud.IP Uni Oldenburg
University of Oldenburg
09.12.2021 14:58:26
inf458 - Term Rewriting Systems (Complete module description)
Original version English Download as PDF
Module label Term Rewriting Systems
Module code inf458
Credit points 6.0 KP
Workload 180 h
Institute directory Department of Computing Science
Applicability of the module
  • Master's Programme Computing Science (Master) > Theoretische Informatik
  • Master's Programme Embedded Systems and Microrobotics (Master) > Akzentsetzungsmodule
Responsible persons
Habel, Annegret (Authorized examiners)
Lehrenden, Die im Modul (Authorized examiners)
Skills to be acquired in this module
The objectives of this module are an introduction to (term) rewriting systems, termination and confluence, the undecidable sets of termination and confluence problems, verifcation procedures of termination and confluence

Professional competence
The students:
  • describe the basics of term rewriting systems
  • characterise the undecidability of termination and confluence problems
  • describe verification procedures of termination and confluence

Methodological competence
The students:
  • apply verification procedures of termination and confluence
  • apply Huet’s completion procedure

Social competence
The students:
  • solve problems in a team
  • present and discuss their results

The students:
  • reflect their actions with regard to term rewriting systems and the methods of those
Module contents
The module is an introduction to term rewriting systems and provides verification procedures for termination and confluence.
Term rewriting systems, termination and confluence are introduced, the undecidability of termination and confluence problems and the decidability for a set of special term rewriting systems are shown.
For this purpose reduction and simplification orders, critical pairs, orthogonality and Huet's completion procedure are introduced, examined and combined.
Reader's advisory
  • Franz Baader, Tobias Nipkow: Term Rewriting and All That. Cambridge University Press, Cambridge 1998.
  • Terese: Term Rewriting Systems, Cambridge University Press, Cambridge, 2003.
Language of instruction German
Duration (semesters) 1 Semester
Module frequency im 2-Jahres-Zyklus
Module capacity unlimited
Reference text
Modullevel / module level AC (Aufbaucurriculum / Composition)
Modulart / typ of module je nach Studiengang Pflicht oder Wahlpflicht
Lehr-/Lernform / Teaching/Learning method
Vorkenntnisse / Previous knowledge
Course type Comment SWS Frequency Workload of compulsory attendance
3 WiSe 42
1 WiSe 14
Total time of attendance for the module 56 h
Examination Time of examination Type of examination
Final exam of module
At the end of the lecture period
exercises and oral or written exam