@article{beeson2022,
	author = {Michael Beeson},
	date-added = {2021-03-12 08:22:28 -0800},
	date-modified = {2022-07-26 23:14:54 -0700},
	journal = {The American Mathematical Monthly},
	number = {7},
	pages = {623-646},
	title = {{E}uclid after computer proof-checking},
	url_pdf = {euclid2020.pdf},
	volume = {129},
	year = {2022}}

@article{beeson2020,
	author = {Michael Beeson},
	date-added = {2020-08-14 13:03:53 -0700},
	date-modified = {2022-07-26 23:09:14 -0700},
	journal = {{B}eitr\"age zur {A}lgebra und {G}eometrie},
	month = {July},
	title = {On the Notion of Equal Figures in {E}uclid},
	url_pdf = {EqualFigures.pdf},
	year = {2022}}

@article{beeson2021b,
	author = {Michael Beeson},
	date-added = {2021-07-21 14:25:57 -0700},
	date-modified = {2021-07-21 14:28:37 -0700},
	title = {The {C}hurch numbers in {N}{F} set theory},
	url_pdf = {nf.pdf},
	year = {2021}}

@article{beeson2021,
	author = {Michael Beeson},
	date-added = {2021-03-23 13:15:55 -0700},
	date-modified = {2021-03-23 14:55:22 -0700},
	title = {Intuitionistic {NF} set theory},
	url_pdf = {inf-basics.pdf},
	year = {2021}}

@article{beeson-triangletiling3,
	author = {Michael Beeson},
	date-added = {2019-02-28 15:08:55 -0800},
	date-modified = {2021-03-23 13:15:42 -0700},
	note = {Available on ArXiv},
	title = {Triangle Tiling: the case $3\alpha + 2\beta = \pi$},
	url_pdf = {TriangleTiling3.pdf},
	year = {2019}}

@article{beeson-isosceles,
	author = {Michael Beeson},
	date-added = {2019-02-28 15:06:04 -0800},
	date-modified = {2021-03-23 13:15:30 -0700},
	note = {Available on ArXiv},
	title = {Tilings of an isosceles triangle},
	url_pdf = {IsoscelesTilings.pdf},
	year = {2019}}

@article{beeson-equilateral,
	author = {Michael Beeson},
	date-added = {2019-02-28 15:04:12 -0800},
	date-modified = {2021-03-23 13:15:16 -0700},
	note = {Available on ArXiv},
	read = {1},
	title = {Tiling an equilateral triangle},
	url_pdf = {TriangleTilingEquilateral.pdf},
	year = {2019}}

@article{beeson2019,
	author = {Michael Beeson and Julien Narboux and Freek Wiedijk},
	date-added = {2018-05-26 01:28:07 +0000},
	date-modified = {2019-02-28 15:04:56 -0800},
	doi = {10.1007/s10472-018-9606-x},
	issn = {1573-7470},
	journal = {Annals of Mathematics and Artificial Intelligence},
	month = {January},
	number = {2},
	pages = {213-257},
	title = {Proof-Checking {E}uclid},
	url = {https://doi.org/10.1007/s10472-018-9606-x},
	url_pdf = {ProofCheckingEuclid.pdf},
	volume = {85},
	year = {2019},
	bdsk-url-1 = {https://doi.org/10.1007/s10472-018-9606-x}}

@article{beeson2019a,
	author = {Michael Beeson},
	date-added = {2018-11-25 10:28:35 -0800},
	date-modified = {2018-11-25 10:30:38 -0800},
	note = {Available on ArXiv},
	title = {No triangle can be cut into seven congruent triangles},
	url_pdf = {NoSevenTiling.pdf},
	year = {2018}}

@article{beeson2018a,
	author = {Michael Beeson},
	date-added = {2016-11-19 15:57:58 +0000},
	date-modified = {2018-01-29 08:31:31 +0000},
	journal = {Indagationes Mathematicae},
	pages = {483-533},
	title = {{B}rouwer and {E}uclid},
	url_pdf = {BrouwerEuclid.pdf},
	volume = {29},
	year = {2018}}

@article{beeson2017a,
	author = {Michael Beeson and Larry Wos},
	date-added = {2015-10-06 19:33:01 +0000},
	date-modified = {2017-03-09 05:40:12 +0000},
	journal = {Journal of Automated Reasoning},
	month = {January},
	number = {1},
	pages = {181-207},
	title = {Finding Proofs in {T}arskian Geometry},
	url_pdf = {Tarski-JAR.pdf},
	volume = {58},
	year = {2017}}

@article{beeson2016a,
	author = {Michael Beeson},
	date-added = {2014-12-13 00:01:19 +0000},
	date-modified = {2015-06-04 18:20:43 +0000},
	journal = {Journal of Formalized Reasoning},
	number = {1},
	pages = {71-99},
	title = {Mixing Computations and Proofs},
	url_pdf = {ProofAndComputation.pdf},
	volume = {9},
	year = {2016}}

@article{beeson2016b,
	author = {Michael Beeson},
	date-added = {2014-11-15 01:19:41 +0000},
	date-modified = {2016-06-08 22:16:45 +0000},
	journal = {Bulletin of Symbolic Logic},
	keywords = {Logic, Geometry, Constructive mathematics},
	month = {March},
	number = {1},
	pages = {1-104},
	title = {Constructive geometry and the parallel postulate},
	url_pdf = {ConstructiveGeometryAndTheParallelPostulate.pdf},
	volume = {22},
	year = {2016}}

@article{beeson2015c-narboux-boutry,
	author = {Michael Beeson and Pierre Boutry and Julien Narboux},
	date-added = {2014-11-15 01:23:10 +0000},
	date-modified = {2015-06-25 19:08:05 +0000},
	journal = {Bulletin of Symbolic Logic},
	keywords = {Logic, Geometry},
	month = {June},
	number = {1},
	pages = {111-122},
	title = {{H}erbrand's theorem and non-{E}uclidean geometry},
	url_pdf = {HerbrandEuclid.pdf},
	volume = {21},
	year = {2015}}

@article{beeson2015b,
	author = {Michael Beeson},
	date-added = {2014-11-15 01:21:33 +0000},
	date-modified = {2015-10-08 17:57:18 +0000},
	doi = {10.1016/j.apal.2015.07.006},
	journal = {Annals of Pure and Applied Logic},
	keywords = {Constructive mathematics, Geometry, Logic},
	number = {11},
	pages = {1199-1273},
	title = {A constructive version of {T}arski's geometry},
	url_pdf = {ConstructiveTarski.pdf},
	volume = {166},
	year = {2015},
	bdsk-url-1 = {http://dx.doi.org/10.1016/j.apal.2015.07.006}}

@article{beeson2015,
	author = {Michael Beeson},
	date-added = {2014-11-15 01:14:46 +0000},
	date-modified = {2019-10-15 11:55:06 -0700},
	howpublished = {ArXiv},
	keywords = {Minimal surfaces},
	title = {A real analytic {J}ordan curve cannot bound infinitely many relative minima of area},
	url_pdf = {part3.pdf},
	year = {2015}}

@inproceedings{beeson2014-wos,
	author = {Michael Beeson and Larry Wos},
	booktitle = {7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, Vienna, Austria, July 19-22, 2014, Proceedings},
	date-added = {2014-11-13 22:38:34 +0000},
	date-modified = {2018-01-29 08:27:18 +0000},
	editor = {St{\'e}phane Demri and Deepak Kapur and Christoph Weidenbach},
	keywords = {Geometry, Automated deduction},
	pages = {495-510},
	publisher = {Springer},
	series = {Lecture Notes in Computer Science},
	title = {OTTER proofs in {T}arskian geometry},
	url_pdf = {TarskiFormalization.pdf},
	volume = {8562},
	year = {2014}}

@inproceedings{beeson2013,
	address = {Berlin Heidelberg},
	author = {Michael Beeson},
	booktitle = {Automated Deduction in Geometry (ADG 2012)},
	date-added = {2014-11-13 22:54:27 +0000},
	date-modified = {2014-11-14 18:30:43 +0000},
	editor = {Tetsuo Ida and Jacques Fleuriot},
	keywords = {Geometry, Constructive mathematics},
	pages = {1-30},
	publisher = {Springer-Verlag},
	series = {Springer Lecture Notes in Artificial Intelligence},
	title = {Proof and Computation in Geometry},
	url_pdf = {Edinburgh.pdf},
	volume = {7993},
	year = {2013}}

@inproceedings{beeson2012,
	address = {Berlin Heidelberg},
	author = {Michael Beeson},
	booktitle = {Computability in Europe 2012},
	date-added = {2014-11-13 22:57:33 +0000},
	date-modified = {2014-11-14 18:30:35 +0000},
	editor = {S. Barry Cooper and Anuj Dawar and Benedict Loewe},
	keywords = {Geometry, Constructive mathematics},
	pages = {46-55},
	publisher = {Springer-Verlag},
	series = {Theoretical Computer Science and General Issues},
	title = {Logic of ruler and compass constructions},
	url_pdf = {Cambridge.pdf},
	volume = {7318},
	year = {2012}}

@incollection{beeson2011,
	author = {Michael Beeson and Jay Halcomb and Wolfgang Mayer},
	booktitle = {ATE-2011, Automated Theory Engineering, Proceedings of the First Workshop on Automated Theory Engineering, Co-Located with the 23rd International Conference on Automated Deduction Wroclaw, Poland, July 31, 2011},
	date-added = {2014-11-14 22:23:30 +0000},
	date-modified = {2014-11-14 22:31:29 +0000},
	editor = {Peter H{\"o}fner and Annabelle McIver and George Struth},
	keywords = {Automated deduction, PSL},
	pages = {9-19},
	publisher = {CEUR},
	title = {Inconsistencies in the Process Specification Language (PSL)},
	url_pdf = {PSL_Inconsistencies.pdf},
	year = {2011}}

@inproceedings{beeson2010,
	address = {Singapore},
	author = {Michael Beeson},
	booktitle = {Proceedings of the Tenth Asian Logic Colloquium, Kobe, Japan, 2008},
	date-added = {2014-11-13 23:03:00 +0000},
	date-modified = {2014-11-15 01:17:11 +0000},
	editor = {T. Arai and J. Brendle and C.~T.~ Chong and R.~Downey and Q.~Feng and H.~Kikyou and H.~Ono},
	keywords = {Geometry, Constructive mathematics},
	pages = {19-84},
	publisher = {World Scientific},
	title = {Constructive Geometry},
	url_pdf = {ConstructiveGeometryFinalPreprintVersion.pdf},
	year = {2010}}

@article{beeson2006,
	author = {Michael Beeson},
	date-added = {2014-11-13 23:07:51 +0000},
	date-modified = {2014-11-14 18:30:04 +0000},
	journal = {Journal of Automated Reasoning},
	keywords = {Automated deduction},
	number = {4},
	pages = {311-344},
	title = {Mathematical Induction in {O}tter-lambda},
	url_pdf = {induction.pdf},
	volume = {36},
	year = {2006}}

@inproceedings{beeson2005b,
	author = {Michael Beeson},
	booktitle = {LPAR-05 Workshop: Empirically Successful Automated Reasoning in Higher-Order Logic (ESHOL)},
	date-added = {2014-11-17 17:39:30 +0000},
	date-modified = {2014-11-17 18:05:43 +0000},
	editor = {Christoph Benzmueller and John Harrison and Carsten Schuermann},
	keywords = {Logic, Otter},
	note = {The first link leads to a slightly extended version. The second link leads to the entire workshop proceedings},
	title = {Implicit and explicit typing in lambda logic},
	url_pdf = {ImplicitAndExplicitTyping.pdf},
	url_pdf2 = {http://arxiv.org/abs/cs/0601042},
	year = {2005}}

@article{beeson2005-veroff-wos,
	author = {Michael Beeson and Robert Veroff and Larry Wos},
	date-added = {2014-11-13 23:12:48 +0000},
	date-modified = {2014-11-14 18:16:30 +0000},
	journal = {Studia Logica},
	keywords = {Automated deduction, Logic},
	number = {2-3},
	pages = {195-234},
	title = {Double negation elimination in some propositional logics},
	url_pdf = {dn.pdf},
	volume = {80},
	year = {2005}}

@article{beeson2005-wiedijk,
	author = {Michael Beeson and Freek Wiedijk},
	date-added = {2014-11-13 23:11:09 +0000},
	date-modified = {2014-11-14 16:58:28 +0000},
	journal = {Journal of Symbolic Computation},
	keywords = {Logic, Symbolic computation},
	number = {5},
	pages = {523-538},
	title = {The meaning of infinity in calculus and computer algebra systems},
	url_pdf = {LimitTheory.pdf},
	volume = {39},
	year = {2005}}

@incollection{beeson2005,
	address = {Milan},
	author = {Michael Beeson},
	booktitle = {Essays on the Foundations of Mathematics and Logic},
	date-added = {2014-11-13 23:09:07 +0000},
	date-modified = {2014-11-14 18:16:21 +0000},
	keywords = {Logic, Constructive mathematics},
	publisher = {Polimetrica},
	title = {Constructivity, computability, and the continuum},
	url_pdf = {ccc.pdf},
	volume = {2},
	year = {2005}}

@inproceedings{beeson2004b,
	author = {Michael Beeson},
	booktitle = {Proceedings of the ESFOR workshop at IJCAR 2004},
	date-added = {2014-11-17 17:33:33 +0000},
	date-modified = {2014-11-17 17:37:46 +0000},
	editor = {Geoff Sutcliffe and Stephan Schulz and Tanel Tammet},
	keywords = {Automated deduction, Otter},
	title = {Otter-lambda, a theorem-prover with untyped lambda-unification},
	url_pdf = {esfor.pdf},
	year = {2004}}

@inproceedings{beeson2004,
	author = {Michael Beeson},
	booktitle = {Automated Reasoning: Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings},
	date-added = {2014-11-13 23:14:14 +0000},
	date-modified = {2014-11-17 17:29:15 +0000},
	keywords = {Automated deduction, Lambda calculus, Logic},
	note = {The second link is to the published version; the first link is to a revised and corrected version.},
	pages = {460-474},
	series = {Lecture Notes in Artificial Intelligence},
	title = {Lambda Logic},
	url_pdf = {LambdaLogic.pdf},
	url_pdf2 = {LambdaLogicOriginal.pdf},
	volume = {3097},
	year = {2004}}

@incollection{beeson2003,
	address = {Berlin Heidelberg New York},
	author = {Michael Beeson},
	booktitle = {Alan Turing: Life and Legacy of a Great Thinker},
	date-added = {2014-11-13 23:16:55 +0000},
	date-modified = {2014-11-14 18:15:34 +0000},
	editor = {Christopher Teuscher},
	keywords = {Automated deduction},
	pages = {77-134},
	publisher = {Springer-Verlag},
	title = {The mechanization of mathematics},
	url_pdf = {turing2.pdf},
	year = {2003}}

@inproceedings{beeson2002b,
	address = {Linz, Austria},
	author = {Michael Beeson},
	booktitle = {LMCS 2002. Logic, Mathematics and Computer Science: Interactions. Symposium in Honor of Bruno Buchberger's 60th Birthday},
	date-added = {2014-11-17 16:42:13 +0000},
	date-modified = {2014-11-17 18:05:05 +0000},
	editor = {Koji Nakagawa},
	keywords = {Otter, Unification, Automated deduction},
	number = {RISC Technical Report 02-60},
	publisher = {RISC},
	title = {Solving for functions},
	url_pdf = {http://www.michaelbeeson.com/research/papers/SolvingForFunctions.pdf},
	year = {2002}}

@article{beeson2002a,
	author = {Michael Beeson},
	date-added = {2014-11-14 19:22:39 +0000},
	date-modified = {2014-11-17 18:09:15 +0000},
	journal = {Sciences et Techniques Educatives},
	keywords = {MathXpert, Education},
	note = {The link is to the English original; I do not have a copy of the French published version.},
	number = {1-2},
	title = {Math{X}pert : un logiciel pour aider les {\'e}l{\`e}ves {\`a} apprendre les math{\'e}matiques par l'action},
	url_pdf = {English-ste.pdf},
	volume = {9},
	year = {2002}}

@inproceedings{beeson2002-wiedijk,
	author = {Michael Beeson and Freek Wiedijk},
	booktitle = {Artificial Intelligence, Automated Reasoning, and Symbolic Computation: Joint International Conferences, AISC 2002 and Calculemus 2002, Marseille, France, July 2002, Proceedings},
	date-added = {2014-11-13 23:20:17 +0000},
	date-modified = {2014-11-14 18:15:19 +0000},
	editor = {Jacques Calmet and Belaid Benhamou and Olga Caprotti and Laurent Henocque and Volker Sorge},
	keywords = {Logic, Symbolic computation},
	pages = {246-258},
	title = {The meaning of infinity in calculus and computer algebra systems},
	year = {2002}}

@inproceedings{beeson2001b,
	author = {Michael Beeson},
	booktitle = {Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 2001, Proceedings},
	date-added = {2014-11-13 23:38:15 +0000},
	date-modified = {2014-11-14 19:30:37 +0000},
	editor = {Rajeev Gore and Alexander Leitsch and Tobias Nipkow},
	keywords = {Automated deduction},
	pages = {318-324},
	publisher = {Springer-Verlag},
	title = {A second-order theorem prover applied to circumscription},
	url_pdf = {circumscription.pdf},
	volume = {2083},
	year = {2001}}

@article{beeson2001,
	author = {Michael Beeson},
	date-added = {2014-11-13 23:28:10 +0000},
	date-modified = {2014-11-14 19:31:28 +0000},
	journal = {Journal of Symbolic Computation},
	keywords = {Automated deduction},
	number = {4},
	pages = {333-349},
	title = {Automatic derivation of the irrationality of e},
	url_pdf = {JSCVersion.pdf},
	volume = {32},
	year = {2001}}

@incollection{beeson1998a,
	address = {Berlin Heidelberg New York},
	author = {Michael Beeson},
	booktitle = {Computer-Human Interaction in Symbolic Computation},
	date-added = {2014-11-13 23:48:07 +0000},
	date-modified = {2018-01-29 08:35:21 +0000},
	editor = {Norman Kajler},
	keywords = {MathXpert, Education},
	pages = {89-115},
	publisher = {Springer-Verlag},
	title = {Design Principles of {M}athpert: Software to support education in algebra and calculus},
	url_pdf = {hisc.pdf},
	year = {1998}}

@inproceedings{beeson1998d,
	address = {Berlin Heidelberg New York},
	author = {Michael Beeson},
	booktitle = {Artificial Intelligence and Symbolic Computation},
	date-added = {2014-11-13 23:35:21 +0000},
	date-modified = {2014-11-14 19:32:10 +0000},
	editor = {Jacques Calmet and Jan Plaza},
	keywords = {Automated deduction},
	pages = {67-83},
	publisher = {Springer-Verlag},
	series = {Lecture Notes in Artificial Intelligence},
	title = {Automatic generation of epsilon-delta proofs of continuity},
	url_pdf = {aisc.pdf},
	volume = {1476},
	year = {1998}}

@inproceedings{beeson1998c,
	author = {Michael Beeson},
	booktitle = {15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings},
	date-added = {2014-11-13 23:31:21 +0000},
	date-modified = {2014-11-14 20:02:58 +0000},
	editor = {Claude Kirchner and Helene Kirchner},
	keywords = {Unification, Automated deduction, Lambda calculus},
	pages = {96-111},
	title = {Unification in lambda calculus with if-then-else},
	url_pdf = {Unify.pdf},
	year = {1998}}

@article{beeson1998b,
	author = {Michael Beeson},
	date-added = {2014-11-13 23:30:24 +0000},
	date-modified = {2014-11-14 20:03:35 +0000},
	journal = {Philosophia Mathematica},
	keywords = {Logic, Constructive mathematics, Philosophy},
	pages = {131-168},
	title = {Reality and Truth in Mathematics},
	url_pdf = {reality.pdf},
	volume = {6},
	year = {1998}}

@misc{beeson1997c,
	author = {Michael Beeson},
	date-added = {2014-11-14 22:41:12 +0000},
	date-modified = {2019-02-28 15:18:01 -0800},
	keywords = {Math{X}pert, Education, Software},
	note = {The current version of this software is sold by Help With Math.},
	publisher = {MathXpert Systems},
	title = {MathXpert Calculus Assistant},
	url_helpwithmath = {http://www.helpwithmath.com},
	year = {1997}}

@misc{beeson1997b,
	author = {Michael Beeson},
	date-added = {2014-11-14 22:39:49 +0000},
	date-modified = {2019-02-28 15:17:51 -0800},
	keywords = {MathXpert, Education, Software},
	note = {The current version of this software is sold by Help With Math.},
	publisher = {MathXpert Systems},
	title = {Math{X}pert Precalculus Assistant},
	url_helpwithmath = {http://www.helpwithmath.com},
	year = {1997}}

@misc{beeson1997a,
	author = {Michael Beeson},
	date-added = {2014-11-14 22:36:22 +0000},
	date-modified = {2019-02-28 15:17:40 -0800},
	keywords = {MathXpert, Education, Software},
	note = {The current version of this software is sold by Help With Math.},
	publisher = {MathXpert Systems},
	title = {Math{X}pert Algebra Assistant},
	url_helpwithmath = {http://www.helpwithmath.com},
	year = {1997}}

@article{beeson1995,
	author = {Michael Beeson},
	date-added = {2014-11-13 23:45:44 +0000},
	date-modified = {2014-11-14 20:05:39 +0000},
	journal = {International Journal of Foundations of Computer Science},
	keywords = {Logic, MathXpert, Nonstandard analysis},
	number = {3},
	pages = {299-338},
	title = {Using nonstandard analysis to verify the correctness of computations},
	url_pdf = {nsappt.pdf},
	volume = {6},
	year = {1995}}

@article{beeson1992a,
	author = {Michael Beeson},
	date-added = {2014-11-13 23:54:43 +0000},
	date-modified = {2014-11-14 20:07:17 +0000},
	journal = {American Mathematical Monthly},
	keywords = {Geometry},
	number = {3},
	pages = {243-252},
	title = {Triangles with vertices on lattice points},
	url_pdf = {triangle.pdf},
	volume = {99},
	year = {1992}}

@inproceedings{beeson1992b,
	author = {Michael Beeson},
	booktitle = {Logic Programming and Automated Reasoning},
	date-added = {2014-11-13 23:52:44 +0000},
	date-modified = {2014-11-14 21:59:02 +0000},
	editor = {A.~ Voronkov},
	keywords = {MathXpert, Symbolic computation, Education},
	pages = {454-457},
	series = {Lecture Notes in Artificial Intelligence},
	title = {{M}athpert: Computer support for learning algebra, trigonometry, and calculus},
	volume = {624},
	year = {1992}}

@inproceedings{beeson1992c,
	address = {Vienna},
	author = {Michael Beeson},
	booktitle = {Proceedings of the International Wittgenstein Symposium on Philosophy of Mathematics, Aug. 16-22, 1992},
	date-added = {2014-11-13 23:50:51 +0000},
	date-modified = {2014-11-14 20:06:33 +0000},
	editor = {J. Czermak},
	keywords = {Logic, Constructive mathematics},
	publisher = {Wittgenstein Society},
	title = {Constructivism in the Nineties},
	url_pdf = {const92.pdf},
	year = {1992}}

@incollection{beeson1991,
	author = {Michael Beeson},
	booktitle = {Extensions of Logic Programming},
	date-added = {2014-11-14 21:57:08 +0000},
	date-modified = {2019-10-15 11:47:36 -0700},
	editor = {P. Schroeder-Heister},
	keywords = {Proof theory, Automated deduction},
	pages = {101-156},
	publisher = {Springer-Verlag},
	series = {Lecture Notes in Computer Science},
	title = {Some applications of {G}entzen's proof theory to automated deduction},
	url_pdf = {Gentzen.pdf},
	volume = {475},
	year = {1991}}

@article{beeson1990,
	author = {Michael Beeson},
	date-added = {2014-11-14 21:55:49 +0000},
	date-modified = {2014-11-14 21:56:52 +0000},
	journal = {Journal of Artificial Intelligence and Education},
	keywords = {MathXpert, Education},
	pages = {65-76},
	title = {A computerized environment for learning algebra, trigonometry, and calculus},
	volume = {1},
	year = {1990}}

@incollection{beeson1989c,
	address = {Berlin Heidelberg New York},
	author = {Michael Beeson},
	booktitle = {Computers and Mathematics '89},
	date-added = {2014-11-14 21:54:16 +0000},
	date-modified = {2014-11-14 21:55:33 +0000},
	keywords = {MathXpert, Logic, Computation},
	pages = {202-214},
	publisher = {Springer-Verlag},
	title = {Logic and computation in {M}athpert: An expert system for learning mathematics},
	year = {1989}}

@inproceedings{beeson1989b,
	address = {Amsterdam},
	author = {Michael Beeson},
	booktitle = {Artificial Intelligence and Education '89},
	date-added = {2014-11-14 21:52:19 +0000},
	date-modified = {2014-11-14 21:53:46 +0000},
	editor = {Bierman and Breuker and Sandberg},
	keywords = {MathXpert, Education},
	pages = {9-14},
	publisher = {IOS},
	title = {The user model in {M}athpert, an expert system for learning mathematics},
	year = {1989}}

@inproceedings{beeson1989a,
	author = {Michael Beeson},
	booktitle = {Proceedings of the Conference on Technology in Collegiate Mathematics Education, Columbus, Ohio, October, 1988},
	date-added = {2014-11-14 21:49:58 +0000},
	date-modified = {2014-11-14 21:54:11 +0000},
	keywords = {MathXpert, Education},
	pages = {9-14},
	publisher = {Addison-Wesley},
	title = {{M}athpert: An expert system for learning mathematics},
	year = {1989}}

@article{beeson1988b,
	author = {Michael Beeson},
	date-added = {2014-11-14 21:47:14 +0000},
	date-modified = {2014-11-14 21:48:38 +0000},
	journal = {Theoretical Computer Science},
	keywords = {Logic, Set theory, Symbolic computation},
	pages = {297-340},
	title = {Towards a computation system based on set theory,},
	url_pdf = {beeson1988b.pdf},
	volume = {60},
	year = {1988}}

@incollection{beeson1988a,
	author = {Michael Beeson},
	booktitle = {The Universal Turing Machine: A Half-Century Survey},
	date-added = {2014-11-14 21:44:47 +0000},
	date-modified = {2014-11-14 21:48:56 +0000},
	editor = {R. Herken},
	keywords = {Logic, Computation},
	note = {Second edition, Springer-Verlag (1994)},
	publisher = {Oxford University Press},
	title = {Computerizing Mathematics: Logic and Computation},
	year = {1988}}

@incollection{beeson1987,
	address = {Providence, R.~I.},
	author = {Michael Beeson},
	booktitle = {Logic and Computation},
	date-added = {2014-11-14 21:43:00 +0000},
	date-modified = {2014-11-14 21:44:29 +0000},
	keywords = {Logic, Constructive mathematics},
	publisher = {American Mathematical Society},
	series = {Contemporary Mathematics},
	title = {Some theories conservative over intuitionistic arithmetic},
	volume = {106},
	year = {1987}}

@inproceedings{beeson1986,
	author = {Michael Beeson},
	booktitle = {Logic, Methodology, and Philosophy of Science VII, proceedings of the International Congress, Salzburg, 1983},
	date-added = {2014-11-14 21:40:22 +0000},
	date-modified = {2014-11-14 21:49:25 +0000},
	editor = {Ruth Barcus and Marcus and Dorn and Weingartner},
	keywords = {Logic, Computation},
	note = {This paper has been translated into French and Russian.},
	pages = {51-81},
	title = {Proving programs and programming proofs},
	year = {1986}}

@article{beeson1985b,
	author = {Michael Beeson},
	date-added = {2014-11-14 16:50:41 +0000},
	date-modified = {2014-11-17 18:13:34 +0000},
	journal = {Pacific Journal of Mathematics},
	keywords = {Minimal surfaces},
	note = {The second link gives comments (written 2006) that simplify the proof and answer a question raised by Nitsche.},
	pages = {17-25},
	title = {The $6\pi$ theorem in minimal surfaces},
	url_pdf = {sixpi.pdf},
	url_pdf2 = {sixpiReview.pdf},
	volume = {117},
	year = {1985}}

@book{beeson1985a,
	address = {Berlin Heidelberg New York Tokyo},
	author = {Michael Beeson},
	date-added = {2014-11-14 16:48:13 +0000},
	date-modified = {2019-02-28 15:14:25 -0800},
	keywords = {Logic, Constructive mathematics},
	number = {6},
	publisher = {Springer},
	series = {Ergebnisse der Mathematik und ihrer Grenzgebiete},
	title = {Foundations of Constructive Mathematics: Metamathematical Studies},
	year = {1985}}

@article{beeson1984-scedrov,
	author = {Michael Beeson and Andre Scedrov},
	date-added = {2014-11-14 16:53:41 +0000},
	date-modified = {2014-11-14 18:11:38 +0000},
	journal = {Journal of Symbolic Logic},
	keywords = {Logic, Constructive mathematics},
	pages = {273-308},
	title = {Church's thesis, continuity, and set theory},
	volume = {49},
	year = {1984}}

@article{beeson1984-tromba,
	author = {Michael Beeson and Anthony J. Tromba},
	date-added = {2014-11-14 16:52:15 +0000},
	date-modified = {2018-02-13 00:48:28 +0000},
	journal = {Manuscripta Mathematica},
	keywords = {Minimal surfaces},
	pages = {273-308},
	title = {The cusp catastrophe of {T}hom in the bifurcation of minimal surfaces},
	volume = {46},
	year = {1984}}

@article{beeson1982b,
	author = {Michael Beeson},
	date-added = {2014-11-14 21:38:25 +0000},
	date-modified = {2014-11-14 22:10:52 +0000},
	journal = {Mathematische Zeitschrift},
	keywords = {Minimal surfaces},
	pages = {1-30},
	title = {Some results on finiteness in {P}lateau's problem, Part {II}},
	volume = {181},
	year = {1982}}

@inproceedings{beeson1982c,
	address = {Amsterdam},
	author = {Michael Beeson},
	booktitle = {Logic Colloquium '80},
	date-added = {2014-11-14 21:03:24 +0000},
	date-modified = {2014-11-14 22:13:45 +0000},
	editor = {Dirk van Dalen and D.~Lascar and J.~Smiley},
	keywords = {Logic, Constructive mathematics},
	pages = {11-55},
	publisher = {North-Holland},
	title = {Problematic principles in constructive mathematics},
	year = {1982}}

@article{beeson1982a,
	author = {Michael Beeson},
	date-added = {2014-11-14 16:55:21 +0000},
	date-modified = {2014-11-14 18:11:32 +0000},
	journal = {Annals of Mathematical Logic},
	keywords = {Logic, Constructive mathematics, Proof theory},
	pages = {127-178},
	title = {Recursive models for constructive set theories},
	volume = {23},
	year = {1982}}

@inproceedings{beeson1981,
	author = {Michael Beeson},
	booktitle = {Constructive Mathematics, Proceedings, New Mexico, 1980},
	date-added = {2014-11-14 17:19:41 +0000},
	date-modified = {2014-11-14 18:11:16 +0000},
	editor = {Fred Richman},
	keywords = {Logic, Constructive mathematics},
	pages = {146-191},
	series = {Lecture Notes in Mathematics},
	title = {Formalizing constructive mathematics: why and how?},
	volume = {873},
	year = {1981}}

@article{beeson1980c,
	author = {Michael Beeson},
	date-added = {2014-11-14 21:01:14 +0000},
	date-modified = {2014-11-14 21:02:51 +0000},
	journal = {Pacific Journal of Mathematics},
	keywords = {Logic, Constructive mathematics},
	pages = {1-28},
	title = {Extensionality and choice in constructive mathematics},
	volume = {88},
	year = {1980}}

@article{beeson1980b,
	author = {Michael Beeson},
	date-added = {2014-11-14 17:04:19 +0000},
	date-modified = {2014-11-14 22:10:41 +0000},
	journal = {Mathematische Zeitschrift},
	keywords = {Minimal surfaces},
	pages = {103-122},
	title = {Some results on finiteness in {P}lateau's problem, Part {I}},
	volume = {175},
	year = {1980}}

@article{beeson1980a,
	author = {Michael Beeson},
	date-added = {2014-11-14 17:02:06 +0000},
	date-modified = {2014-11-14 18:11:05 +0000},
	journal = {Mathematische Zeitschrift},
	keywords = {Minimal surfaces},
	pages = {103-123},
	title = {On interior branch points of minimal surfaces},
	volume = {175},
	year = {1980}}

@inproceedings{beeson1979b,
	address = {Amsterdam},
	author = {Michael Beeson},
	booktitle = {Logic Colloquium '78},
	date-added = {2014-11-14 17:14:38 +0000},
	date-modified = {2014-11-14 18:10:55 +0000},
	editor = {M.~Boffa and Dirk van Dalen and D.~Lascar and J.~Smiley},
	keywords = {Logic, Constructive mathematics},
	publisher = {North-Holland},
	title = {Continuity in intuitionistic set theories},
	year = {1979}}

@article{beeson1979a,
	author = {Michael Beeson},
	date-added = {2014-11-14 17:13:46 +0000},
	date-modified = {2014-11-14 18:10:48 +0000},
	journal = {Pacific Journal of Mathematics},
	keywords = {Logic, Constructive mathematics},
	pages = {1-16},
	title = {Goodman's theorem and beyond},
	volume = {84},
	year = {1979}}

@article{beeson1978b,
	author = {Michael Beeson},
	date-added = {2014-11-17 16:37:21 +0000},
	date-modified = {2014-11-17 18:04:36 +0000},
	journal = {Journal of Symbolic Logic},
	keywords = {Constructive mathematics, Logic},
	pages = {228-246},
	title = {Some relations between classical and constructive mathematics},
	volume = {43},
	year = {1978}}

@article{beeson1978a,
	author = {Michael Beeson},
	date-added = {2014-11-14 17:00:54 +0000},
	date-modified = {2014-11-17 16:37:19 +0000},
	journal = {Journal of Symbolic Logic},
	keywords = {Logic, Constructive mathematics, Proof theory},
	pages = {213-227},
	title = {A type-free {G}{\"o}del interpretation},
	volume = {43},
	year = {1978}}

@article{beeson1977c,
	author = {Michael Beeson},
	date-added = {2014-11-14 17:12:47 +0000},
	date-modified = {2014-11-14 18:10:08 +0000},
	journal = {Pacific Journal of Mathematics},
	keywords = {Minimal surfaces},
	pages = {11-17},
	title = {Non-continuous dependence of surfaces of least area on the boundary curve},
	year = {1977}}

@article{beeson1977b,
	author = {Michael Beeson},
	date-added = {2014-11-14 17:11:54 +0000},
	date-modified = {2014-11-14 18:09:59 +0000},
	journal = {Annals of Mathematical Logic},
	keywords = {Logic, Constructive mathematics},
	pages = {249-322},
	title = {Principles of continuous choice and continuity of functions in formal systems for constructive mathematics},
	year = {1977}}

@article{beeson1977a,
	author = {Michael Beeson},
	date-added = {2014-11-14 17:10:43 +0000},
	date-modified = {2014-11-14 18:09:54 +0000},
	journal = {Pacific Journal of Mathematics},
	keywords = {Logic, Constructive mathematics},
	pages = {29-40},
	title = {Continuity and comprehension in intuitionistic formal systems},
	volume = {68},
	year = {1977}}

@article{beeson1977d,
	author = {Michael Beeson},
	date-added = {2014-11-14 16:56:55 +0000},
	date-modified = {2014-11-14 18:10:25 +0000},
	journal = {Archive of Rational Mechanics and Analysis},
	keywords = {Minimal surfaces},
	pages = {213-227},
	title = {The behavior of a minimal surface in a corner},
	volume = {65},
	year = {1977}}

@article{beeson1976b,
	author = {Michael Beeson},
	date-added = {2014-11-14 17:08:25 +0000},
	date-modified = {2014-11-14 18:09:41 +0000},
	journal = {Journal of Symbolic Logic},
	keywords = {Logic, Constructive mathematics},
	pages = {28-24},
	title = {The unprovability in intuitionistic formal systems of the continuity of effective operations on the reals},
	volume = {41},
	year = {1976}}

@article{beeson1976a,
	author = {Michael Beeson},
	date-added = {2014-11-14 17:07:04 +0000},
	date-modified = {2014-11-14 18:09:32 +0000},
	journal = {Journal of Symbolic Logic},
	keywords = {Logic, Constructive mathematics},
	pages = {321-346},
	title = {The non-derivability in intuitionistic formal systems of theorems on the continuity of effective operations},
	volume = {40},
	year = {1976}}

@article{beeson1976c,
	author = {Michael Beeson},
	date-added = {2014-11-14 17:05:56 +0000},
	date-modified = {2014-11-14 18:09:47 +0000},
	journal = {Journal of Symbolic Logic},
	keywords = {Logic, Constructive mathematics},
	pages = {328-336},
	title = {Derived rules of inference related to the continuity of effective operations},
	volume = {41},
	year = {1976}}

@phdthesis{beeson1972,
	author = {Michael Beeson},
	date-added = {2014-11-14 17:09:32 +0000},
	date-modified = {2014-11-14 18:09:23 +0000},
	keywords = {Logic, Constructive mathematics},
	school = {Stanford},
	title = {The metamathematics of constructive theories of effective operations},
	year = {1972}}