Introduction to unification theory. (English) Zbl 0704.68096

Formal techniques in artificial intelligence, Stud. Comput. Sci. Artif. Intell. 6, 369-424 (1990).
[For the entire collection see Zbl 0704.68001.]
It is useless to support the importance of the unification theory in artificial intelligence fields and, actually, in computer science. The present paper represents a tutorial introduction to this topic, discussing some fundamental and most recent results. The issues in Section 3, which is the main part of the paper, are: first-order unification, unification in equational (associative, commutative, distributive) theories, unification in order sorted logics and logic programming languages, unification-based grammars, higher-order unification, complexity results on matching and unification algorithms, universal unification.
A consistent bibliography of 236 titles is contained.
Reviewer: N.Curteanu


68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68W30 Symbolic computation and algebraic computation


Zbl 0704.68001