This expository paper on the development of automated reasoning tools is a must read for anyone interested in knowing more about this area. In particular, the paper discusses the automated reasoning program OTTER, which was developed at Argonne Labs. Many of OTTER’s successes, including the solution to the Robbins problem, are presented. The paper outlines some of the reasoning strategies OTTER uses to arrive at its conclusions.