The notebooks provide detailed accounts of the original and highly successful approaches Wos takes to the problems of finding proofs of new results in logic and mathematics, and to proof refinement--the discovery of shorter and more elegant proofs than can be found elsewhere in the literature. The main tool used is William McCune’s program OTTER, but Wos’s strategies can be employed with automated reasoning programs generally. Each of the notebooks presents various ideas, challenges, and open questions that suggest topics for further research and so can serve as a source of inspiration for those seeking new avenues for investigation and diverse problems in various areas. Neither expertise in automated reasoning nor in the area in focus is required to understand the contents of a given notebook.