6th International School on Rewriting
July 16th - 20th, 2012. Valencia, Spain
MUG: Matching, Unification, and Generalizations
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.
