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.
Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, United Kingdom, 1998.
Franz Baader and Jörg Siekmann. Unification Theory. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, pages 41-125. Oxford University Press, Oxford, UK, 1994.
Franz Baader and Wayne Snyder. Unification Theory. In J.A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, pages 447-533. Elsevier Science Publishers, 2001.
Jean-Pierre Jouannaud, Claude Kirchner: Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification. Computational Logic - Essays in Honor of Alan Robinson 1991: 257-321.
