2 citations · 2 across the 4 of their papers we have counts for
5 papers
Finding Proofs in Tarskian Geometry
Michael Beeson, Larry Wos
We report on a project to use a theorem prover to find proofs of the theorems in Tarskian geometry. These theorems start with fundamental properties of betweenness, proceed through…
Double-Negation Elimination in Some Propositional Logics
Michael Beeson, Robert Veroff, Larry Wos
This article answers two questions (posed in the literature), each concerning the guaranteed existence of proofs free of double negation. A proof is free of double negation if none…
XCB, the Last of the Shortest Single Axioms for the Classical Equivalential Calculus
Larry Wos, Dolph Ulrich, Branden Fitelson
It has long been an open question whether the formula XCB = EpEEEpqErqr is, with the rules of substitution and detachment, a single axiom for the classical equivalential calculus.…
Vanquishing the XCB Question: The Methodology Discovery of the Last Shortest Single Axiom for the Equivalential Calculus
Larry Wos, Dolph Ulrich, Branden Fitelson
With the inclusion of an effective methodology, this article answers in detail a question that, for a quarter of a century, remained open despite intense study by various researche…
A Spectrum of Applications of Automated Reasoning
Larry Wos
The likelihood of an automated reasoning program being of substantial assistance for a wide spectrum of applications rests with the nature of the options and parameters it offers o…