A Machine Program for Theorem-Proving The program of a proof procedure is discussed in connection with trial runs and possible improvements. CACM July, 1962 Davis, M. Logemann, G. Loveland, D. CA620724 JB March 17, 1978 8:11 PM 537 5 537 537 5 537 537 5 537