Solving Equational Problems: Matching and Unification
Course at ISR 2017, 9th International School on Rewriting
July 3–7, 2017. Eindhoven, The Netherlands.

Overview Slides Literature Lecturer

Matching and unification are two fundamental operations, necessary to perform a step in reduction or to generate a critical pair in completion. Their application areas are wide ranging, including not only rewriting, but also automated theorem proving, programming, computational linguistics, software engineering, etc.
The goal of the course is two-fold. On the one hand, it aims at refreshing and deepening participants’ knowledge in basic matching and unification algorithms. On the other hand, it will help them to better understand more advanced topics related to equational unification and matching. We will start with the first-order syntactic case, then will discuss general results about equational unification and matching, and, at the end, will look in more detail at solving associative-commutative unification problems. At the end of each topic, the participants will be given exercises to practice in the class.

Slides can be downloaded from here.

Literature, Links

Temur Kutsia
Research Institute for Symbolic Computation
Johannes Kepler University Linz

Back to the teaching page