Michael Beeson

Publication Activity (10 Years)

Years Active: 1975-2022
Publications (10 Years): 9

Top Topics

Consistency Checking

Theorem Proving

Top Venues

Bull. Symb. Log.

J. Autom. Reason.

Ann. Math. Artif. Intell.

Publications

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