# zbMATH — the first resource for mathematics

Designing unification procedures using transformations: A survey. (English) Zbl 0744.68112
Introduction: We shall focus on unification problems arising in methods for automated theorem proving. This covers at least the kind of unification arising in resolution and $$E$$-resolution (S. A. Robinson [J. Assoc. Comput. Mach. 12, 23–41 (1965; Zbl 0139.12303)], G. Plotkin [Machine Intell. 7, 73–90 (1972; Zbl 0262.68036)]), matings (P. Andrews [J. Assoc. Comput. Math. 28(2), 193–214 (1981; Zbl 0456.68119)], W. Bibel [Theor. Comput. Sci. 8, 31–44 (1979; Zbl 0421.03011); J. Assoc. Comput. Mach. 28, 633–645 (1981; Zbl 0468.68097); Automated theorem proving. Braunschweig: Friedr. Vieweg & Sohn (1982; Zbl 0492.68027)]), equational matings, (J. H. Gallier, P. Narendran, D. Plaisted and W. Snyder [Inf. Comput. 87, No. 1–2, 129–195 (1990; Zbl 0709.68080); Theorem proving using equational matings and rigid $$E$$-unification, J. Assoc. Comput. Mach. 39, No. 2, 377–429 (1992; Zbl 0799.68171)]), and $$ET$$-proofs (F. Pfenning [Proof transformations in higher-order logic, Ph. D. thesis, Department of Mathematics, Carnegie Mellon University, Pittsburgh/PA (1987)], D. Miller [Proofs in higher-order logic, Ph. D. thesis, Carnegie-Mellon University (1983); Stud. Logica 46, 347–370 (1987; Zbl 0644.03033)]).
The topics that we will cover are:
$$\bullet$$ $$E$$-unification ($$E$$ a finite set of first-order equations).
$$\bullet$$ Rigid $$E$$-unification ($$E$$ a finite set of first-order equations), a decidable form of $$E$$-unification recently introduced in the framework of Andrews and Bibel’s method of matings.
$$\bullet$$ Higher-order unification (in the simply-typed $$\lambda$$- calculus).
All three unification problems will be tackled using the method of transformations on term systems, already anticipated in J. Herbrand’s [Sur la théorie de la démonstration, Logical Writings, Cambridge (1971)], and revived very effectively by A. Martelli and U. Montanari [ACM Trans. Program. Lang. and Syst. 4, 258–282 (1982; Zbl 0478.68093)] for standard unification. In a nutshell, the method is as follows:
A unification problem is gradually transformed into one whose solution is (almost) obvious.

##### MSC:
 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 68W30 Symbolic computation and algebraic computation 68N17 Logic programming 68-02 Research exposition (monographs, survey articles) pertaining to computer science
##### Keywords:
unification; resolution; matings; equational matings; $$ET$$-proofs