LOGIC & COMPUTATION 42

Unification procedures arising in methods for automated theorem proving based on matings are surveyed. We begin by reviewing some fundamentals of automated deduction, including the Skolem form and the Skolem-Herbrand-Gödel theorem. Next, the method of matings for first-order languages without equality due to Andrews and Bibel is presented. Standard unification is described in terms of transformations on systems (following the approach of Martelli and Montanari, anticipated by Herbrand). Some fast unification algorithms are also sketched, in particular, a unification closure algorithm inspired by Paterson and Wegman's method. The method of matings is then extended to languages with equality. This extention leads naturally to a generalization of standard unification called rigid E-unification (due to Gallier, Narendran, Plaisted, and Snyder). The main properties of rigid E-unification, decidability, NP-completeness, and finiteness of complet