MUG: Matching, Unification, Generalizations
Course at ISR 2012, 6th International School on Rewriting
July 16th - 20th, 2012. Valencia, Spain.

Overview Slides and Exercises Literature Lecturer

The purpose of this course is to give an overview on syntactic matching and unification and their generalizations to the equational case.
Matching and unification are equation solving techniques that play an essential role in term rewriting. Matching problems arise at each rewrite step, to decide whether a term is an instance of another term. Unification problems are to be solved in the process of computation of critical pairs. Equational matching and unification are very useful in rewriting modulo an equational theory and in rewriting-based deduction. We discuss syntactic algorithms, their properties, ways of their efficient implementation, and specific equational theories.

Slides and Exercises


Temur Kutsia
Research Institute for Symbolic Computation
Johannes Kepler University of Linz
Altenbergerstrasse 69
A-4040 Linz, Austria
+43 (0)732 2468 9982 (phone)
+43 (0)732 2468 9930 (fax)

Back to the teaching page