Introduction to Unification Theory

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 course covering the following topics: syntactic unification, Robinson's algorithm, improved algorithms for syntactic unification (space efficient, quadratic, almost linear), unification in equational theories, higher-order unification, matching, applications of unification.

Students are expected to present a selected topic in the class. There will be also homework assignments.

Number:	326.010
Title:	Unification Theory
Lecturer:	Temur Kutsia
Time:	TBA
Place:	TBA
Language:	English
First meeting:	March 9, at 17:15 in T112
Registration:	Via the KUSSS system.

• Syntactic unification.
• Improved algorithms for syntactic unification.
• Equational unification.
• Narrowing.
• Higher-order unification.
• Applications.

• 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.
• Claude Kirchner and Hélène Kirchner. Rewriting, Solving, Proving.
• Kevin Knight. Unification: A Multidisciplinary Survey. ACM Computing Surveys, 21(1), 1989.
• R. Ramesh, I. V. Ramakrishnan. Nonlinear pattern matching in trees. Journal of the ACM 39(2), pages 295-316, 1992.
• Wayne Snyder and Jean Gallier. Higher-Order Unification Revisited: Complete Sets of Transformations. Journal of Symbolic Computation 8(1/2), pages 101-140, 1989.