Automated Theorem Proving 1965–1970

In this article we give a critical history of automated theorem proving from 1965 through 1970. By evaluating the contributions of the period, we provide a guide to a study of the field during its development. In order to differentiate between that work which turned out to be significant and that which had lesser impact, we occasionally rely of necessity on developments occurring after 1970. Since we confine our attention to automated theorem proving, certain work in logic occurring in the period in question is ignored. For example, various studies on decidability and complexity are excluded from comment because they are not directly germane. In addition to providing a critique, we have the secondary objective of giving a tutorial. We provide sufficient information and definition to permit one to read this article with minimal recourse to the literature. In this regard we often replace the very rigorous treatment of a concept by a more intuitive description.