You are here

Rewriting General Course for Beginners


Lecturer: Aart Middeldorp. University of Innsbruck, Austria
(basic track, 13 lecture sessions, 5 exercise sessions)

This course provides a modern introduction to term rewriting, a Turing-complete computational model based on directed equations. We discuss basic concepts, algorithms and results. Exercise sessions familiarize the participants with the presented material. The course is concluded with an outlook to some recent research in term rewriting.

The following topics will be covered:

  • Introduction (motivation, equational reasoning, rewriting).
  • Abstract rewriting (basic notions, relationships, Newman's lemma).
  • Equational reasoning (terms, semantics, matching).
  • Term rewriting (Turing-completeness, combinatory logic, undecidability).
  • Termination (polynomial interpretations, lexicographic path order, Knuth-Bendix order, dependency pairs).
  • Completion (unification, critical pairs, normalization equivalence).
  • Confluence (orthogonality, decreasing diagrams).
  • Strategies (normalization, strategy annotations).
  • Advanced topics (modern termination techniques, complexity, conditional rewriting, modularity, Gröbner bases, tree automata techniques).

No background knowledge is assumed.

Here's some supporting material (username and password will be given at the start of the conference).