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 at the Seventh International Tbilisi Summer School in Logic and Language is structured into two lectures of introductory level covering the following topics: syntactic unification, Robinson's algorithm, improved algorithms for syntactic unification (space efficient, quadratic, almost linear), application.
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 and Claude Kirchner. Solving Equations in Abstract Algebras. A Rule-Based Survey on Unification. In Jean-Louis Lassez and Gordon Plotkin, editors. Computational Logic. Essays in Honor of A. Robinson. MIT Press, 1991.
Claude Kirchner (ed.). Unification. Academic Press, London, 1990.
Jean-Louis Lassez, Michael Maher, and Kim Marriott. Unification revisited. In Jeff Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 587-625. Morgan Kaufman, 1987.