Michael Beeson

41 papers A 4B 1C 1Misc 2Journal 26Unranked 4
YearRankTypeTitle / Venue / Authors
2022 J jnl
Euclid after Computer Proof-Checking.
Am. Math. Mon.
Michael Beeson
2022 J jnl
Larry Wos: Visions of Automated Reasoning.
J. Autom. Reason.
Michael Beeson, Maria Paola Bonacina, Michael Kinyon, Geoff Sutcliffe
2020 J jnl
On the Notion of Equal Figures in Euclid.
CoRR
Michael Beeson
2019 J jnl
Proof-checking Euclid.
Ann. Math. Artif. Intell.
Michael Beeson, Julien Narboux, Freek Wiedijk
2017 J jnl
Finding Proofs in Tarskian Geometry.
J. Autom. Reason.
Michael Beeson, Larry Wos
2017 J jnl
Proof-checking Euclid.
CoRR
Michael Beeson, Julien Narboux, Freek Wiedijk
2016 J jnl
Constructive Geometry and the Parallel postulate.
Bull. Symb. Log.
Michael Beeson
2016 J jnl
Finding Proofs in Tarskian Geometry.
CoRR
Michael Beeson, Larry Wos
2016 J jnl
Mixing Computations and Proofs.
J. Formaliz. Reason.
Michael Beeson
2015 J jnl
A constructive version of Tarski's geometry.
Ann. Pure Appl. Log.
Michael Beeson
2015 J jnl
Herbrand's Theorem and non-Euclidean Geometry.
Bull. Symb. Log.
Michael Beeson, Pierre Boutry, Julien Narboux
2014 A conf
OTTER Proofs in Tarskian Geometry.
IJCAR
Michael Beeson, Larry Wos
2012 C conf
Logic of Ruler and Compass Constructions.
CiE
Michael Beeson
2012 — conf
Proof and Computation in Geometry.
Automated Deduction in Geometry
Michael Beeson
2011 — conf
Inconsistencies in the Process Specification Language (PSL).
ATE
Michael Beeson, Jay Halcomb, Wolfgang Mayer
2006 J jnl
A Tour through Mathematical Logic by Robert S. Wolf.
Am. Math. Mon.
Michael Beeson
2006 J jnl
Mathematical Induction in Otter-Lambda.
J. Autom. Reason.
Michael Beeson
2006 — ch.
Otter/Ivy.
The Seventeen Provers of the World
Michael Beeson, William McCune
2005 J jnl
Double-Negation Elimination in Some Propositional Logics.
Stud Logica
Michael Beeson, Robert Veroff, Larry Wos
2005 J jnl
The meaning of infinity in calculus and computer algebra systems.
J. Symb. Comput.
Michael Beeson, Freek Wiedijk
2004 A conf
Lambda Logic.
IJCAR
Michael Beeson
2003 J jnl
Double-Negation Elimination in Some Propositional Logics
CoRR
Michael Beeson, Robert Veroff, Larry Wos
2002 Misc conf
The Meaning of Infinity in Calculus and Computer Algebra Systems.
AISC
Michael Beeson, Freek Wiedijk
2001 A conf
A Second-Order Theorem Prover Applied to Circumscription.
IJCAR
Michael Beeson
2001 J jnl
Automatic Derivation of the Irrationality of e.
J. Symb. Comput.
Michael Beeson
1999 — conf
Automatic derivation of the irrationality of e.
Calculemus
Michael Beeson
1998 Misc conf
Automatic Generation of Epsilon-Delta Proofs of Continuity.
AISC
Michael Beeson
1998 — ch.
Design principles of Mathpert: software to support education in algebra and calculus.
Computer-Human Interaction in Symbolic Computation
Michael Beeson
1998 — ch.
Erratum to: Algorithm animation with Agat.
Computer-Human Interaction in Symbolic Computation
Michael Beeson
1998 A conf
Unification in Lambda-Calculi with if-then-else.
CADE
Michael Beeson
1995 J jnl
Using Nonstandard Analysis to Ensure the Correctness of Symbolic Computations.
Int. J. Found. Comput. Sci.
Michael Beeson
1992 B conf
Mathpert: Computer Support for Learning Algebra, Trig, and Calculus.
LPAR
Michael Beeson
1989 — conf
Some Applications of Gentzen's Proof Theory in Automated Deduction.
ELP
Michael Beeson
1988 J jnl
Towards a Computation System Based on Set Theory.
Theor. Comput. Sci.
Michael Beeson
1984 J jnl
Church's Thesis, Continuity, and Set Theory.
J. Symb. Log.
Michael Beeson, Andre Scedrov
1982 J jnl
Recursive models for constructive set theories.
Ann. Math. Log.
Michael Beeson
1978 J jnl
A Type-Free Godel Interpretation.
J. Symb. Log.
Michael Beeson
1978 J jnl
Some Relations Between Classical and Constructive Mathematics.
J. Symb. Log.
Michael Beeson
1976 J jnl
Derived Rules of Inference Related to the Continuity of Effective Operations.
J. Symb. Log.
Michael Beeson
1976 J jnl
The Unprovability in Intuitionistic Formal Systems of the Continuity of Effective Operations on the Reals.
J. Symb. Log.
Michael Beeson
1975 J jnl
The Nonderivability in Intuitionistic Formal Systems of Theorems on the Continuity of Effective Operations.
J. Symb. Log.
Michael Beeson