Journal of the ACM, 1965. Minor soiling from the removal of an address label. A very good, clean copy. Wrappers. Octavo. Item #10646
Automated theorem proving was discussed and triied since Jevons built his logic machine in 1870. However, the theory became a reality only when Robinson showed the completeness of the resolution principle and its compatibility with machine operations.