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, type inference, rewriting and completion, 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.

Number:	326.097, 326.0UF
Title:	Unification Theory
Lecturer:	Temur Kutsia
Time:	Tuesday, 15:30-17:00
Place:	K 012D
Language:	English
First meeting:	March 11
Registration:	Via the KUSSS system.
Exam:	Tuesday, July 1, 15:30-17:00, in K 012D.

• Syntactic unification. Slides, to print.
• Improved algorithms for syntactic unification. Slides, to print.
• Matching. Slides, to print.
• Equational unification. Slides, to print.
• Narrowing. Slides.
• Systems of linear Diophantine equations. Slides, to print.
• Higher-order unification. Slides, to print.
• Applications. Slides, to print.

• 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.
• Christian Prehofer, "Solving Higher-Order Equations: From Logic to Programming", Birkhäuser PTCS Series, 1997.
• 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.