7 A Partial Mechanization of Second-order Logic J. L. Darlington

Spectra 70 / 46 and the IBM 360/50, that performs many second-order inferences in addition to carrying out first-order'resolutions' on Skolemized disjunctive formulae. The second-order aspect of the program is represented by an extended matching procedure, which operates in conjunction with rules for lambda abstraction and application, and for existential generalization and instantiation. These rules abstract properties from first-order formulae and apply axioms such as mathematical induction to these properties, thereby generating new second-order formulae as well as first-order formulae that could not have been produced by the resolution method alone. The mechanization of second-order logic is of potential usefulness in the areas of deductive question answering, illustrated by an example, and to the proving of formal properties of programs. Among the more interesting recent developments in the theory and practice of automatic theorem proving are the incorporation of formal techniques such as J. A. Robinson's resolution method into the'deductive sections' of question-answering and problem-solving systems (Chadwick et al. 1969, Green 1969), the solution of previously'open' problems (Guard et a/.