Automated Reasoning, by Larry Wos, Ph.D.

Home PagebulletAbout Automated Reasoning bulletOtter Theorem Prover  

Are you looking for a thesis topic for your Ph.D?
Are you, instead, looking for some problem to solve that, if successful, might result in a publication?
Are you looking for challenges, intrigue, and excitement?
The notebooks you will find on this website, in the form of pdfs, will offer you, I believe, much pleasure.
If you enjoy puzzle solving where a computer program played a major role, these notebooks might indeed be just what you would enjoy.
Each features results of research, in general not published elsewhere.
Each notebook is quite readable, not requiring you to be an expert.
Please feel free to contact me by E–mail, especially if you have a proof that you wish to be made more elegant.

Notebook PDFs
A Surprising Story of Research Discoveries: How Significant Advances for Automated Reasoning Occurred

Hilbertís 24th Problem, Proof Simplification, and Automated Reasoning

An Amazing Approach to Plane Geometry

Unearthing Gold: Groups, Semigroups, and Unsolved Problems.

Hunting Treasure in Intuitionism

Future Enhancements for Automated Reasoning Programs

Exploring Algebra in Search of Elegant Proofs

An Astonishing Discovery from Proof Shortening: The Fecundity of the BCI Logic

Discovering New Theorems: A Study of Extensions of the BCSK Logic

Proof Shortening: What's the Point?

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

The Subformula Strategy: Coping with Complex Expressions

A Startling Result, Some Challenges Met, but Some Still Remain: More Coping with Complex Expressions

Some Interesting Experiments: A Study of Lukasiewicz's Infinite-Valued Sentential Calculus

A Prelude to Unveiling Some of the Mysteries of Proof Discovery: A Study of the BCSK Logic.
Larry Wos, Ph.D. All rights reserved.
graphical design - binary