Unification theory

AbstractMost knowledge based systems in artificial intelligence (AI), with a commitment to asymbolic representation, support one basic operation: “matching of descriptions”. This operation, called unification in work on deduction, is the “addition-and-multiplication” of AI-systems and is consequently often supported by special purpose hardware or by a fast instruction set on most AI-machines. Unification theory provides the formal framework for investigations into the properties of this operation. This article surveys what is presently known in unification theory and records its early history