Unification Theory
Franz Baader, Jörg H Siekrnann · 1994
Abstract Most knowledge-based systems in artificial intelligence (AI) with a commitment to a symbolic representation support one important operation: ‘matching of descriptions’. This operation, called unification in the field of deduction systems, is the ‘addition and multiplication’ of many AI systems, and is consequently often supported by special purpose hardware or by a fast instruction set. Unification theory provides the formal framework for investigations into the properties of this operation, which is in essence the solving of equations in an (equationally defined) free algebra.