inf458 - Term Rewriting Systems (Complete module description)

Module label	Term Rewriting Systems
Modulkürzel	inf458
Credit points	6.0 KP
Workload	180 h
Institute directory	Department of Computing Science
Verwendbarkeit des Moduls	Master's Programme Computing Science (Master) > Theoretische Informatik
Zuständige Personen	Lehrenden, Die im Modul (module responsibility) Lehrenden, Die im Modul (Prüfungsberechtigt)
Prerequisites	No participant requirements
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 Self-competence 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.
Literaturempfehlungen	Franz Baader, Tobias Nipkow: Term Rewriting and All That. Cambridge University Press, Cambridge, 1998. Terese: Term Rewriting Systems, Cambridge University Press, Cambridge, 2003.
Links
Language of instruction	German
Duration (semesters)	1 Semester
Module frequency	in a 2-year cycle
Module capacity	unlimited
Reference text	Blockveranstaltung
Teaching/Learning method	1VL + 1Ü
Previous knowledge	none

Lehrveranstaltungsform	SWS	Frequency	Workload of compulsory attendance
Lecture	3	WiSe	42
Exercises	1	WiSe	14
Präsenzzeit Modul insgesamt			56 h

Examination	Prüfungszeiten	Type of examination
Final exam of module	At the end of the lecture period	exercises and oral or written exam