Introduction

Most researchers consider the modern period of automated logic to have begun with the discovery of resolution by J.A. Robinson in 1963 at the Argonne National Laboratory. Previously, it was known by the Herbrand-Skolem-Godel theorem that semi-decision procedures could be designed for first-order logic by reducing the question of the unsatisfiability of a set of first-order formulae to the question of unsatisfiability of (roughly) a set of certain ground formulae derived from the original set in an effective way (for example, see [32]). But until Robinson invented the simple and powerful inference rule known as resolution [139], no practically efficient semi-decision procedure had been found. The crucial component of this seminal discovery was in fact the rediscovery by Robinson of the process of unification, which had been discovered by Herbrand in his thesis 33 years earlier (see Appendix 3).1