Bachelor Program - Term Rewriting
VU3 SS 2026 703141
News
Check this site regularly for announcements; visit the content section to access the slides and lecture notes.
Overview
Lecturers
| Type | Lecturer | Room | Consultation Hours |
| VU | Aart Middeldorp | 3M07 | Monday, 12:00 - 13:30 |
| VU | Philipp Dablander | 3M03 | Wednesday, 10:00 - 11:30 |
Time & Place
The course starts on March 2nd.
Monday 15:30 – 18:00 HS 11
Language
The course is taught in English.
Registration
Online registration is required until 23:59 on February 21st.
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.
Schedule
| Week | Date | Topics | Slides | Solutions |
| 1 | 02.03 | examples, terms, matching algorithm | PDF (1x1, 4x1) | |
| 2 | 09.03 | abstract rewrite systems, Newman's lemma | PDF (1x1, 4x1) | |
| 3 | 16.03 | multiset orders, equational reasoning, algebras | PDF (1x1, 4x1) | |
| 4 | 23.03 | term rewrite systems, undecidability | PDF (1x1, 4x1) | |
| 5 | 13.04 | congruence closure, termination, polynomial interpretations | PDF (1x1, 4x1) | |
| 6 | 20.04 | LPO, unification, critical pairs | PDF (1x1, 4x1) | |
| 7 | 27.04 | completion, first-order theory of rewriting | PDF (1x1, 4x1) | |
| 8 | 04.05 | KBO, normalization equivalence, abstract completion | PDF (1x1, 4x1) | |
| 9 | 11.05 | confluence, orthogonality | PDF (1x1, 4x1) | |
| 10 | 18.05 | proof terms, strategies, normalization | PDF (1x1, 4x1) | |
| 11 | 01.06 | strategy annotations, simple termination | PDF (1x1, 4x1) | |
| 12 | 08.06 | dependency pairs, Z property | PDF (1x1, 4x1) | |
| 13 | 15.06 | dependency pairs | PDF (1x1, 4x1) | |
| 14 | 22.06 | test |
Literature
The course material and slides will be made available online. The same holds for solutions to selected exercises.
Course Material
- Lecture notes (version of 28th February 2026)
Additional Material
Lecture 2
- Original proof of Newman's lemma
- Interesting article about Max Newman
Lecture 5
Termination Tools
Lecture 8
Harald Zankl, Nao Hirokawa and Aart Middeldorp, KBO Orientability, Journal of Automated Reasoning 43(2), pp. 173 – 201, 2009
Completion Tools
- KBCV
- Maxcomp
- mkbTT
- WaldmeisterWaldmeister