Ronald Sklar - Computational logic: 1950's-1965

The idea of mechanizing mathematics can be traced back to Descartes and Leibniz. But the first truly automated proofs in mathematics had to wait until the 1950s and the invention of the electronic computer. The purpose of this talk is to trace the use of logic in automated deduction with particular emphasis on the use of the principle of resolution. Along the way the contributions and ideas of Descartes, Leibniz, Skolem, Herbrand, Hilbert and Ackermann, Gödel, Church, Turing, Davis and Putnam, J. A. Robinson and others will be briefly discussed.