Content

In this course a number of current and advanced topics in term rewriting is covered:

• conditional term rewriting
• confluence criteria
• context-sensitive rewriting
• proof terms
• strategies
• …

Basic knowledge of term rewriting (as covered in the bachelor course Term Rewriting) is assumed. Access to the recordings of the 2020 version of the bachelor course Term Rewriting is provided to interested students.

Schedule

week	date	topics	slides	solutions	material
1	06.03	review of bachelor course	pdf (1x1, 4x1)	pdf	lecture notes
2	13.03	critical pair conditions, proof terms	pdf (1x1, 4x1)	pdf	link
3	20.03	proof terms	pdf (1x1, 4x1)	pdf	link
4	27.03	proof terms	pdf (1x1, 4x1)	pdf	link
5	17.04	Hydra battles, semantic labeling	pdf (1x1, 4x1)	pdf	link
6	24.04	semantic labeling, AC rewriting	pdf (1x1, 4x1)	pdf
7	08.05	ordinals, AC termination	pdf (1x1, 4x1)	pdf	link
8	15.05	AC termination, conditional rewriting	pdf (1x1, 4x1)	pdf	link
9	22.05	conditional termination	pdf (1x1, 4x1)	pdf
10	05.06	conditional confluence, transformations	pdf (1x1, 4x1)	pdf
11	12.06	dependency pairs	pdf (1x1, 4x1)	pdf
12	19.06	AC termination	pdf (1x1, 4x1)
13	26.06	test (solution)

Literature

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