6th International School on Rewriting >> Matching, Unification, and Generalizations

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.

<< Back to Previous Page.