The Nonderivability in Intuitionistic Formal Systems of Theorems on the Continuity of Effective Operations. - Michael Beeson (J. Symb. Log., 1975)

The Unprovability in Intuitionistic Formal Systems of the Continuity of Effective Operations on the Reals. - Michael Beeson (J. Symb. Log., 1976)

Derived Rules of Inference Related to the Continuity of Effective Operations. - Michael Beeson (J. Symb. Log., 1976)

A Type-Free Godel Interpretation. - Michael Beeson (J. Symb. Log., 1978)

Some Relations Between Classical and Constructive Mathematics. - Michael Beeson (J. Symb. Log., 1978)

Recursive models for constructive set theories. - Michael Beeson (Ann. Math. Log., 1982)

Church's Thesis, Continuity, and Set Theory. - Michael Beeson; Andre Scedrov (J. Symb. Log., 1984)

Towards a Computation System Based on Set Theory. - Michael Beeson (Theor. Comput. Sci., 1988)

Some Applications of Gentzen's Proof Theory in Automated Deduction. - Michael Beeson (ELP, 1989)

Mathpert: Computer Support for Learning Algebra, Trig, and Calculus. - Michael Beeson (LPAR, 1992)

Using Nonstandard Analysis to Ensure the Correctness of Symbolic Computations. - Michael Beeson (Int. J. Found. Comput. Sci., 1995)

Design principles of Mathpert: software to support education in algebra and calculus. - Michael Beeson (Computer-Human Interaction in Symbolic Computation, 1998)

Erratum to: Algorithm animation with Agat. - Michael Beeson (Computer-Human Interaction in Symbolic Computation, 1998)

Automatic Generation of Epsilon-Delta Proofs of Continuity. - Michael Beeson (AISC, 1998)

Unification in Lambda-Calculi with if-then-else. - Michael Beeson (CADE, 1998)

Automatic derivation of the irrationality of e. - Michael Beeson (Calculemus, 1999)

A Second-Order Theorem Prover Applied to Circumscription. - Michael Beeson (IJCAR, 2001)

Lambda Logic. - Michael Beeson (IJCAR, 2004)

The meaning of infinity in calculus and computer algebra systems. - Michael Beeson; Freek Wiedijk (J. Symb. Comput., 2005)

Double-Negation Elimination in Some Propositional Logics. - Michael Beeson; Robert Veroff; Larry Wos (Stud Logica, 2005)

Otter/Ivy. - Michael Beeson; William McCune (The Seventeen Provers of the World, 2006)

Mathematical Induction in Otter-Lambda. - Michael Beeson (J. Autom. Reason., 2006)

A Tour through Mathematical Logic by Robert S. Wolf. - Michael Beeson (Am. Math. Mon., 2006)

Inconsistencies in the Process Specification Language (PSL). - Michael Beeson; Jay Halcomb; Wolfgang Mayer (ATE, 2011)

Proof and Computation in Geometry. - Michael Beeson (Automated Deduction in Geometry, 2012)

Logic of Ruler and Compass Constructions. - Michael Beeson (CiE, 2012)

OTTER Proofs in Tarskian Geometry. - Michael Beeson; Larry Wos (IJCAR, 2014)

A constructive version of Tarski's geometry. - Michael Beeson (Ann. Pure Appl. Log., 2015)

Herbrand's Theorem and non-Euclidean Geometry. - Michael Beeson; Pierre Boutry; Julien Narboux (Bull. Symb. Log., 2015)

Constructive Geometry and the Parallel postulate. - Michael Beeson (Bull. Symb. Log., 2016)

Mixing Computations and Proofs. - Michael Beeson (J. Formaliz. Reason., 2016)

Finding Proofs in Tarskian Geometry. - Michael Beeson; Larry Wos (J. Autom. Reason., 2017)

Proof-checking Euclid. - Michael Beeson; Julien Narboux; Freek Wiedijk (Ann. Math. Artif. Intell., 2019)

On the Notion of Equal Figures in Euclid. - Michael Beeson (CoRR, 2020)

Larry Wos: Visions of Automated Reasoning. - Michael Beeson; Maria Paola Bonacina; Michael Kinyon; Geoff Sutcliffe (J. Autom. Reason., 2022)

Euclid after Computer Proof-Checking. - Michael Beeson (Am. Math. Mon., 2022)