Automated Reasoning, by Larry Wos, Ph.D.

About Automated ReasoningbulletNotebooks bulletOtter Theorem Prover  

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

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. He would also enjoy hearing from anyone who develops and implements one of the program enhancements he suggests in his most recent notebook Future Enhancements for Automated Reasoning Programs.

Recent Notebooks
A Surprising Story of Research Discoveries: How Significant Advances for Automated Reasoning Occurred
A Primer for Automated Reasoning: Puzzles, People, and Programs That Involve Reasoning
An Amazing Approach to Plane Geometry After More Than Thirty-Five Years, Success
Unearthing Gold: Groups, Semigroups, and Unsolved Problems
Hunting Treasure in Intuitionism
Exploring Algebra in Search of Elegant Proofs
The Joy of Solving a Decades–Old Mystery: Success with the BCK and BCI Logics
Full Notebook Collection...
Larry Wos, Ph.D. All rights reserved.
graphical design - binary