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.

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