Unification, or solving equations, is a fundamental process
in many areas of computer science. It is in the heart of the
applications such as logic programming, automated reasoning,
natural language processing, information retrieval, rewriting
and completion, type checking, etc.
The course on Unification Theory is intended to be an introductory
one-week course structured into four lectures to cover the following
topics: syntactic unification, Robinson's algorithm, improved
algorithms for syntactic unification (space efficient, quadratic,
almost linear), higher-order unification, applications of unification.
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.
Gilles Dowek. Higher-Order Unification and Matching. In J.A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, pages 1009-1062. Elsevier Science Publishers, 2001.
Claude Kirchner (ed.). Unification. Academic Press, London, 1990.