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
Lecture 1. July 19, 15:00-17:00. Syntactic Matching and Unification. Slides,
1-up,
2-up,
4-up.
Lecture 2. July 20, 17:30-19:00. Equational Matching and Unification. Slides,
1-up,
2-up,
4-up.
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.