Introduction to Unification Theory

Overview

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.

Students are expected to present a selected topic in the class. There will be also homework assignments. The assessment will be based on participation, assignments, and presentation.

Organization

Summer Semester 2012.

Number:	326.010, 326.IUT
Title:	Unification Theory
Lecturer:	Temur Kutsia
Time:	Wednesday, 15:30-17:00
Place:	S2 059 (Science Park, Second Building)
Language:	English
First meeting:	March 7
Registration:	Via the KUSSS system.

Course Materials

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

Exercises

Exercise set 1.

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&eacuml;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.