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) pdf confluence tools
10 05.12 strategies, normalization pdf (1x1, 4x1) pdf
11 12.12 strategy annotations, simple termination pdf (1x1, 4x1) pdf
12 09.01 dependency pairs, Z property pdf (1x1, 4x1) pdf
13 16.01 matrix interpretations, derivational complexity pdf (1x1, 4x1) pdf complexity tools
14 23.01 completion modulo AC, test practice pdf (1x1, 4x1)
15 30.01 test


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