Term Rewriting
Content: 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.03 | examples, terms, matching algorithm | pdf (1x1, 4x1) | lecture notes | |
| 2 | 10.03 | abstract rewrite systems, Newman's lemma | pdf (1x1, 4x1) | link | |
| 3 | 17.03 | multiset orders, equational reasoning, algebras | pdf (1x1, 4x1) | ||
| 4 | 24.03 | term rewrite systems, undecidability | pdf (1x1, 4x1) | ||
| 5 | 31.03 | congruence closure, termination, polynomial interpretations | pdf (1x1, 4x1) | link | |
| 6 | 07.04 | LPO, unification, critical pairs | pdf (1x1, 4x1) | ||
| 7 | 28.04 | completion, first-order theory of rewriting | pdf (1x1, 4x1) | ||
| 8 | 05.05 | KBO, normalization equivalence, abstract completion | pdf (1x1, 4x1) | link | |
| 9 | 12.05 | confluence, orthogonality | pdf (1x1, 4x1) | link | |
| 10 | 19.05 | proof terms, strategies, normalization | pdf (1x1, 4x1) | link | |
| 11 | 26.05 | strategy annotations, simple termination | pdf (1x1, 4x1) | ||
| 12 | 02.06 | dependency pairs, Z property | pdf (1x1, 4x1) | ||
| 13 | 16.06 | dependency pairs | pdf (1x1, 4x1) | ||
| 14 | 23.06 | test (solution) | pdf (1x1, 4x1) |
Literature
The course material and slides will be made available online. The same holds for solutions to selected exercises.
Summer 2025
Bachelor Program
| Course number | Type/hours | Semester | Title |
|---|---|---|---|
| 703026 + 703027 | VO3 + PS2 | SS 2025 | Logic |
| 703083 + 703084 | VO3 + PS2 | SS 2025 | Program Verification |
| 703141 | VU3 | SS 2025 | Term Rewriting |