en | de

Term Rewriting

bachelor program

VU3  WS 2022/2023  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 03.10 examples, terms, matching algorithm pdf (1x1, 4x1) pdf lecture notes
2 10.10 abstract rewrite systems, Newman's lemma pdf (1x1, 4x1) pdf link
3 17.10 multiset orders, equational reasoning, algebras pdf (1x1, 4x1) pdf
4 24.10 term rewrite systems, undecidability pdf (1x1, 4x1) pdf
5 31.10 congruence closure, termination, polynomial interpretations pdf (1x1, 4x1) pdf termination tools
6 07.11 LPO, unification, critical pairs pdf (1x1, 4x1) pdf
7 14.11 completion, first-order theory of rewriting pdf (1x1, 4x1) pdf
8 21.11 KBO, normalization equivalence, abstract completion pdf (1x1, 4x1) pdf completion tools
9 28.11 confluence, orthogonality pdf (1x1, 4x1) confluence tools
10 05.12 strategies, normalization pdf (1x1, 4x1)
11 12.12 strategy annotations, simple termination
12 09.01 dependency pairs, Z property
13 16.01
14 23.01
15 30.01 test


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