en | de

Term Rewriting

bachelor program

VU3  WS 2023/2024  703141


The course provides an introduction to term rewriting. Term rewriting is a general model of computation which has been successfully applied in many areas of computer science. Here one can think of the analysis and implementation of algebraic specifications of abstract data types, the foundations of functional (logic) programming, automated theorem proving, and code optimization in compilers, to name just a few.


week date topics slides solutions material
1 02.10 examples, terms, matching algorithm pdf (1x1, 4x1) pdf lecture notes
2 09.10 abstract rewrite systems, Newman's lemma pdf (1x1, 4x1) pdf link
3 16.10 multiset orders, equational reasoning, algebras pdf (1x1, 4x1) pdf
4 23.10 term rewrite systems, undecidability pdf (1x1, 4x1) pdf
5 30.10 congruence closure, termination, polynomial interpretations pdf (1x1, 4x1) pdf link
6 06.11 LPO, unification, critical pairs pdf (1x1, 4x1) pdf
7 13.11 completion, first-order theory of rewriting pdf (1x1, 4x1) pdf
8 20.11 KBO, normalization equivalence, abstract completion pdf (1x1, 4x1) pdf link
9 27.11 confluence, orthogonality pdf (1x1, 4x1) pdf link
10 04.12 strategies, normalization pdf (1x1, 4x1) pdf
11 11.12 strategy annotations, simple termination pdf (1x1, 4x1) pdf
12 08.01 dependency pairs, Z property pdf (1x1, 4x1) pdf
13 15.01 matrix interpretations, dependency pairs pdf (1x1, 4x1) pdf
14 22.01 derivational complexity, completion modulo AC, test practice pdf (1x1, 4x1)
15 29.01 test (solution)


The course material and slides will be made available online. The same holds for solutions to selected exercises.