Welcome! This website features a series of notebooks presenting some of Larry Wos’s most recent and hitherto unpublished research in automated reasoning, material that is of interest to logicians, mathematicians, teachers, and students as well as to those in the automated reasoning community

		Notebooks Currently Available
		The Joy of Solving a Decades–Old Mystery: Success with the BCK and BCI Logics
		Three Expeditions in Search of Hidden Treasure: New Proofs in Equivalential Calculus
		A Startling Result, Some Challenges Met, but Some Still Remain: More Coping with Complex Expressions
		The Subformula Strategy: Coping with Complex Expressions
		Others Coming Soon

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.

Wos himself welcomes contact by e–mail, especially if one has a proof in hand and has the goal of finding a better proof.