Michael Beeson

According to our database, Michael Beeson authored at least 36 papers between 1975 and 2022.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of three.

2022

Euclid after Computer Proof-Checking.

Michael Beeson

Am. Math. Mon., 2022

Larry Wos: Visions of Automated Reasoning.

Michael Beeson, Maria Paola Bonacina, Michael Kinyon, Geoff Sutcliffe

J. Autom. Reason., 2022

2020

On the Notion of Equal Figures in Euclid.

Michael Beeson

CoRR, 2020

2019

Proof-checking Euclid.

Michael Beeson, Julien Narboux, Freek Wiedijk

Ann. Math. Artif. Intell., 2019

2017

Finding Proofs in Tarskian Geometry.

Michael Beeson, Larry Wos

J. Autom. Reason., 2017

2016

Mixing Computations and Proofs.

Michael Beeson

J. Formaliz. Reason., 2016

Constructive Geometry and the Parallel postulate.

Michael Beeson

Bull. Symb. Log., 2016

2015

Herbrand's Theorem and non-Euclidean Geometry.

Michael Beeson, Pierre Boutry, Julien Narboux

Bull. Symb. Log., 2015

A constructive version of Tarski's geometry.

Michael Beeson

Ann. Pure Appl. Log., 2015

2014

OTTER Proofs in Tarskian Geometry.

Michael Beeson, Larry Wos

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2012

Logic of Ruler and Compass Constructions.

Michael Beeson

Proceedings of the How the World Computes, 2012

Proof and Computation in Geometry.

Michael Beeson

Proceedings of the Automated Deduction in Geometry - 9th International Workshop, 2012

2011

Inconsistencies in the Process Specification Language (PSL).

Michael Beeson, Jay Halcomb, Wolfgang Mayer

Proceedings of the First Workshop on Automated Theory Engineering, 2011

2006

A Tour through Mathematical Logic by Robert S. Wolf.

Michael Beeson

Am. Math. Mon., 2006

Mathematical Induction in Otter-Lambda.

Michael Beeson

J. Autom. Reason., 2006

Otter/Ivy.

Michael Beeson, William McCune

Proceedings of the Seventeen Provers of the World, Foreword by Dana S. Scott, 2006

2005

Double-Negation Elimination in Some Propositional Logics.

Michael Beeson, Robert Veroff, Larry Wos

Stud Logica, 2005

The meaning of infinity in calculus and computer algebra systems.

Michael Beeson, Freek Wiedijk

J. Symb. Comput., 2005

2004

Lambda Logic.

Michael Beeson

Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

2001

A Second-Order Theorem Prover Applied to Circumscription.

Michael Beeson

Proceedings of the Automated Reasoning, First International Joint Conference, 2001

1999

Automatic derivation of the irrationality of e.

Michael Beeson

Proceedings of the Systems for Integrated Computation and Deduction, 1999

1998

Unification in Lambda-Calculi with if-then-else.

Michael Beeson

Proceedings of the Automated Deduction, 1998

Automatic Generation of Epsilon-Delta Proofs of Continuity.

Michael Beeson

Proceedings of the Artificial Intelligence and Symbolic Computation, 1998

Erratum to: Algorithm animation with Agat.

Michael Beeson

Proceedings of the Computer-Human Interaction in Symbolic Computation, 1998

Design principles of Mathpert: software to support education in algebra and calculus.

Michael Beeson

Proceedings of the Computer-Human Interaction in Symbolic Computation, 1998

1995

Using Nonstandard Analysis to Ensure the Correctness of Symbolic Computations.

Michael Beeson

Int. J. Found. Comput. Sci., 1995

1992

Mathpert: Computer Support for Learning Algebra, Trig, and Calculus.

Michael Beeson

Proceedings of the Logic Programming and Automated Reasoning, 1992

1989

Some Applications of Gentzen's Proof Theory in Automated Deduction.

Michael Beeson

Proceedings of the Extensions of Logic Programming, 1989

1988

Towards a Computation System Based on Set Theory.

Michael Beeson

Theor. Comput. Sci., 1988

1984

Church's Thesis, Continuity, and Set Theory.

Michael Beeson, Andre Scedrov

J. Symb. Log., 1984

1982

Recursive models for constructive set theories.

Michael Beeson

Ann. Math. Log., 1982

1978

Some Relations Between Classical and Constructive Mathematics.

Michael Beeson

J. Symb. Log., 1978

A Type-Free Godel Interpretation.

Michael Beeson

J. Symb. Log., 1978

1976

Derived Rules of Inference Related to the Continuity of Effective Operations.

Michael Beeson

J. Symb. Log., 1976

The Unprovability in Intuitionistic Formal Systems of the Continuity of Effective Operations on the Reals.

Michael Beeson

J. Symb. Log., 1976

1975

The Nonderivability in Intuitionistic Formal Systems of Theorems on the Continuity of Effective Operations.

Michael Beeson

J. Symb. Log., 1975