×

Universal unification. (English) Zbl 0547.03011

Automated deduction, Proc. 7th int. Conf., Napa/Calif. 1984, Lect. Notes Comput. Sci. 170, 1-42 (1984).
[For the entire collection see Zbl 0537.00025.]
The paper represents an authorized survey on the theory of first-order unification. After an introduction to the problem and a review of the variety of computer science areas where unification arises (e.g. databases, information retrieval, computer vision, natural language processing, expert systems, computer algebra, programming languages, algebra, computational logic), section II presents the algebraic and logical formal approaches to unification. Decidability, existence and enumeration problems are stated and a hierarchy of the theories is given. Section III is concerned with the (existence and enumeration) problem: Given an equational theory, does there exist an algorithm which enumerates the set of the most general unifiers for two given terms? The results on the above problem or other challenging problems, in the frame of special theories (associative and/or commutative and/or distributive etc.), are exposed. Important subclasses of equational theories and basic results on the properties of the set of the most general unifiers are given. The universal unification algorithm is sketched and it is pointed out that these results represent a unitary view and a practical guide to actual unification algorithm design, within the variety of techniques used to unification algorithms inside different theories. Section IV gives an outlook to the open problems, enunciating 15 of the most interesting ones. An extensive bibliography of 138 basic papers is appended.
Reviewer: N.Curteanu

MSC:

03B35 Mechanization of proofs and logical operations
03C05 Equational classes, universal algebra in model theory
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
08A50 Word problems (aspects of algebraic structures)
03D40 Word problems, etc. in computability and recursion theory
03-02 Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
68-02 Research exposition (monographs, survey articles) pertaining to computer science

Citations:

Zbl 0537.00025