Michael Beeson - researchr alias

researchr

You are not signed in
Sign in
Sign up

Viewing Publication 1 - 37 from 37

2022

Euclid after Computer Proof-CheckingMichael Beeson. tamm, 129(7):623-646, 2022. [doi]

Larry Wos: Visions of Automated ReasoningMichael Beeson, Maria Paola Bonacina, Michael Kinyon, Geoff Sutcliffe. JAR, 66(4):439-461, 2022. [doi]

2019

Proof-checking EuclidMichael Beeson, Julien Narboux, Freek Wiedijk. AMAI, 85(2-4):213-257, 2019. [doi]

2017

Finding Proofs in Tarskian GeometryMichael Beeson, Larry Wos. JAR, 58(1):181-207, 2017. [doi]

2016

Mixing Computations and ProofsMichael Beeson. jfrea, 9(1):71-99, 2016. [doi]

Constructive Geometry and the Parallel postulateMichael Beeson. bsl, 22(1):1-104, 2016. [doi]

2015

A constructive version of Tarski's geometryMichael Beeson. APAL, 166(11):1199-1273, 2015. [doi]

Herbrand's Theorem and non-Euclidean GeometryMichael Beeson, Pierre Boutry, Julien Narboux. bsl, 21(2):111-122, 2015. [doi]

2014

OTTER Proofs in Tarskian GeometryMichael Beeson, Larry Wos. cade 2014: 495-510 [doi]

2012

Logic of Ruler and Compass ConstructionsMichael Beeson. CiE 2012: 46-55 [doi]

Proof and Computation in GeometryMichael Beeson. adg 2013: 1-30 [doi]

2011

Inconsistencies in the Process Specification Language (PSL)Michael Beeson, Jay Halcomb, Wolfgang Mayer. ate 2011: 9-19 [doi]

2006

Otter/IvyMichael Beeson, William McCune. tphol 2006: 36-40 [doi]

Mathematical Induction in Otter-LambdaMichael Beeson. JAR, 36(4):311-344, 2006. [doi]

A Tour through Mathematical Logic by Robert S. WolfMichael Beeson. tamm, 113(3):275-280, 2006. [doi]

2005

The meaning of infinity in calculus and computer algebra systemsMichael Beeson, Freek Wiedijk. JSC, 39(5):523-538, 2005. [doi]

Double-Negation Elimination in Some Propositional LogicsMichael Beeson, Robert Veroff, Larry Wos. sLogica, 80(2-3):195-234, 2005. [doi]

2004

Lambda LogicMichael Beeson. cade 2004: 460-474 [doi]

2002

The Meaning of Infinity in Calculus and Computer Algebra SystemsMichael Beeson, Freek Wiedijk. AISC 2002: 246-258 [doi]

2001

Automatic Derivation of the Irrationality of eMichael Beeson. JSC, 32(4):333-349, 2001.

A Second-Order Theorem Prover Applied to CircumscriptionMichael Beeson. cade 2001: 318-324 [doi]

1999

Automatic derivation of the irrationality of eMichael Beeson. ENTCS, 23(3):420-439, 1999. [doi]

1998

Unification in Lambda-Calculi with if-then-elseMichael Beeson. cade 1998: 103-118 [doi]

Automatic Generation of Epsilon-Delta Proofs of ContinuityMichael Beeson. AISC 1998: 67-83 [doi]

Design principles of Mathpert: software to support education in algebra and calculusMichael Beeson. In Norbert Kajler, editor, Computer-Human Interaction in Symbolic Computation. Texts and Monographs in Symbolic Computation, pages 163-177, Springer, 1998. [doi]

Erratum to: Algorithm animation with AgatMichael Beeson. In Norbert Kajler, editor, Computer-Human Interaction in Symbolic Computation. Texts and Monographs in Symbolic Computation, pages 209, Springer, 1998. [doi]

1995

Using Nonstandard Analysis to Ensure the Correctness of Symbolic ComputationsMichael Beeson. ijfcs, 6(3):299-338, 1995.

1992

Mathpert: Computer Support for Learning Algebra, Trig, and CalculusMichael Beeson. lpar 1992: 454-456

1989

Some Applications of Gentzen s Proof Theory in Automated DeductionMichael Beeson. elp 1991: 101-156

1988

Towards a Computation System Based on Set TheoryMichael Beeson. TCS, 60:297-340, 1988.

1984

Church s Thesis, Continuity, and Set TheoryMichael Beeson, Andre Scedrov. JSYML, 49(2):630-643, 1984.

1982

Recursive models for constructive set theoriesMichael Beeson. APAL, 23(2-3):127-178, 1982. [doi]

1978

Some Relations Between Classical and Constructive MathematicsMichael Beeson. JSYML, 43(2):228-246, 1978.

A Type-Free Godel InterpretationMichael Beeson. JSYML, 43(2):213-227, 1978.

1976

The Unprovability in Intuitionistic Formal Systems of the Continuity of Effective Operations on the RealsMichael Beeson. JSYML, 41(1):18-24, 1976.

Derived Rules of Inference Related to the Continuity of Effective OperationsMichael Beeson. JSYML, 41(2):328-336, 1976.

1975

The Nonderivability in Intuitionistic Formal Systems of Theorems on the Continuity of Effective OperationsMichael Beeson. JSYML, 40(3):321-346, 1975.

Sign in or sign up to see more results.

runs on WebDSL