Unification Theory
Introductory Course at the Third RISC/SCIEnce Training School in Symbolic Computation,
RISC, Castle of Hagenberg, Austria. July 7-20, 2008



Overview Lecture Abstracts and Slides Literature Lecturer

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, 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.

Lectures
Lecture 1. July 8, 200810:45-12:15Syntactic UnificationSlides
Lecture 2. July 8, 200814:00-15:30Improved Algorithms for Syntactic UnificationSlides
Lecture 3. July 10, 200809:00-10:30Higher-Order UnificationSlides
Lecture 4. July 11, 200809:00-10:30ApplicationsSlides

Literature

Lecturer
Temur Kutsia
Research Institute for Symbolic Computation
Johannes Kepler University of Linz
Altenbergerstrasse 69
A-4040 Linz, Austria
+43 (0)732 2468 9982 (phone)
+43 (0)732 2468 9930 (fax)
kutsia@risc.uni-linz.ac.at


Back