Automated Reasoning, by Larry Wos, Ph.D.

About Automated ReasoningbulletNotebooks  
spacer

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

spacer
spacer
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
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
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
Full Notebook Collection...
spacer
Larry Wos, Ph.D. All rights reserved.
graphical design - binary