Introduction to Unification Theory (326.097, 326.0UF)

Unification, or solving equations, is a fundamental process in many areas of computer science. It is in the heart of the applications such as automated reasoning, logic programming, type inference in programming languages, rewriting, 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, anti-unification, and applications.

Number:	326.097, 326.0UF
Title:	Unification Theory
Lecturer:	Temur Kutsia
Time:	Wednesday, 12:00-13:30
Place:	MZ 005B
Language:	English
First meeting:	March 6
Registration:	Via the KUSSS system.

Based on in-class quizzes and presentation.

Please visit the course Moodle page.