UNIFICATION
 ===========

 Temur Kutsia

 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.