\n \n \n
\n
\n \n 2025\n \n \n (1)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n \n Finite sets, mappings, cardinals, and arithmetic in intuitionistic NF.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n . 2025.\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 4 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@article{beeson2025,\n\tauthor = {Michael Beeson},\n\tdate-added = {2021-03-23 13:15:55 -0700},\n\tdate-modified = {2021-03-23 14:55:22 -0700},\n\ttitle = {Finite sets, mappings, cardinals, and arithmetic in intuitionistic {NF}},\n\turl_pdf = {inf-basicsZML.pdf},\n\tyear = {2025}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 2022\n \n \n (2)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n \n Euclid after computer proof-checking.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n
The American Mathematical Monthly, 129(7): 623-646. 2022.\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@article{beeson2022,\n\tauthor = {Michael Beeson},\n\tdate-added = {2021-03-12 08:22:28 -0800},\n\tdate-modified = {2022-07-27 11:03:24 -0700},\n\tdoi = {10.1080/00029890.2022.2069985},\n\tjournal = {The American Mathematical Monthly},\n\tnumber = {7},\n\tpages = {623-646},\n\ttitle = {{E}uclid after computer proof-checking},\n\turl_pdf = {euclid2020.pdf},\n\tvolume = {129},\n\tyear = {2022}}\n\n\n
\n\n\n\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 2021\n \n \n (1)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n \n The Church numbers in NF set theory.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n . 2021.\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@article{beeson2021b,\n\tauthor = {Michael Beeson},\n\tdate-added = {2021-07-21 14:25:57 -0700},\n\tdate-modified = {2021-07-21 14:28:37 -0700},\n\ttitle = {The {C}hurch numbers in {N}{F} set theory},\n\turl_pdf = {nf.pdf},\n\tyear = {2021}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 2019\n \n \n (4)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n \n Triangle Tiling: the case $3α + 2β = π$.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n . 2019.\n
Available on ArXiv\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@article{beeson-triangletiling3,\n\tauthor = {Michael Beeson},\n\tdate-added = {2019-02-28 15:08:55 -0800},\n\tdate-modified = {2021-03-23 13:15:42 -0700},\n\tnote = {Available on ArXiv},\n\ttitle = {Triangle Tiling: the case $3\\alpha + 2\\beta = \\pi$},\n\turl_pdf = {TriangleTiling3.pdf},\n\tyear = {2019}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Tilings of an isosceles triangle.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n . 2019.\n
Available on ArXiv\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@article{beeson-isosceles,\n\tauthor = {Michael Beeson},\n\tdate-added = {2019-02-28 15:06:04 -0800},\n\tdate-modified = {2021-03-23 13:15:30 -0700},\n\tnote = {Available on ArXiv},\n\ttitle = {Tilings of an isosceles triangle},\n\turl_pdf = {IsoscelesTilings.pdf},\n\tyear = {2019}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Tiling an equilateral triangle.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n . 2019.\n
Available on ArXiv\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@article{beeson-equilateral,\n\tauthor = {Michael Beeson},\n\tdate-added = {2019-02-28 15:04:12 -0800},\n\tdate-modified = {2021-03-23 13:15:16 -0700},\n\tnote = {Available on ArXiv},\n\tread = {1},\n\ttitle = {Tiling an equilateral triangle},\n\turl_pdf = {TriangleTilingEquilateral.pdf},\n\tyear = {2019}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Proof-Checking Euclid.\n \n \n \n \n\n\n \n Beeson, M.; Narboux, J.; and Wiedijk, F.\n\n\n \n\n\n\n
Annals of Mathematics and Artificial Intelligence, 85(2): 213-257. January 2019.\n
\n\n
\n\n
\n\n
\n\n \n \n
Paper\n \n \n \n
pdf\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@article{beeson2019,\n\tauthor = {Michael Beeson and Julien Narboux and Freek Wiedijk},\n\tdate-added = {2018-05-26 01:28:07 +0000},\n\tdate-modified = {2019-02-28 15:04:56 -0800},\n\tdoi = {10.1007/s10472-018-9606-x},\n\tissn = {1573-7470},\n\tjournal = {Annals of Mathematics and Artificial Intelligence},\n\tmonth = {January},\n\tnumber = {2},\n\tpages = {213-257},\n\ttitle = {Proof-Checking {E}uclid},\n\turl = {https://doi.org/10.1007/s10472-018-9606-x},\n\turl_pdf = {ProofCheckingEuclid.pdf},\n\tvolume = {85},\n\tyear = {2019},\n\tbdsk-url-1 = {https://doi.org/10.1007/s10472-018-9606-x}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 2018\n \n \n (2)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n \n No triangle can be cut into seven congruent triangles.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n . 2018.\n
Available on ArXiv\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@article{beeson2019a,\n\tauthor = {Michael Beeson},\n\tdate-added = {2018-11-25 10:28:35 -0800},\n\tdate-modified = {2018-11-25 10:30:38 -0800},\n\tnote = {Available on ArXiv},\n\ttitle = {No triangle can be cut into seven congruent triangles},\n\turl_pdf = {NoSevenTiling.pdf},\n\tyear = {2018}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Brouwer and Euclid.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n
Indagationes Mathematicae, 29: 483-533. 2018.\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@article{beeson2018a,\n\tauthor = {Michael Beeson},\n\tdate-added = {2016-11-19 15:57:58 +0000},\n\tdate-modified = {2018-01-29 08:31:31 +0000},\n\tjournal = {Indagationes Mathematicae},\n\tpages = {483-533},\n\ttitle = {{B}rouwer and {E}uclid},\n\turl_pdf = {BrouwerEuclid.pdf},\n\tvolume = {29},\n\tyear = {2018}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 2017\n \n \n (1)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n \n Finding Proofs in Tarskian Geometry.\n \n \n \n \n\n\n \n Beeson, M.; and Wos, L.\n\n\n \n\n\n\n
Journal of Automated Reasoning, 58(1): 181-207. January 2017.\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@article{beeson2017a,\n\tauthor = {Michael Beeson and Larry Wos},\n\tdate-added = {2015-10-06 19:33:01 +0000},\n\tdate-modified = {2017-03-09 05:40:12 +0000},\n\tjournal = {Journal of Automated Reasoning},\n\tmonth = {January},\n\tnumber = {1},\n\tpages = {181-207},\n\ttitle = {Finding Proofs in {T}arskian Geometry},\n\turl_pdf = {Tarski-JAR.pdf},\n\tvolume = {58},\n\tyear = {2017}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 2016\n \n \n (2)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n \n Mixing Computations and Proofs.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n
Journal of Formalized Reasoning, 9(1): 71-99. 2016.\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n\n\n\n
\n
@article{beeson2016a,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-12-13 00:01:19 +0000},\n\tdate-modified = {2015-06-04 18:20:43 +0000},\n\tjournal = {Journal of Formalized Reasoning},\n\tnumber = {1},\n\tpages = {71-99},\n\ttitle = {Mixing Computations and Proofs},\n\turl_pdf = {ProofAndComputation.pdf},\n\tvolume = {9},\n\tyear = {2016}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Constructive geometry and the parallel postulate.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n
Bulletin of Symbolic Logic, 22(1): 1-104. March 2016.\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@article{beeson2016b,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-11-15 01:19:41 +0000},\n\tdate-modified = {2016-06-08 22:16:45 +0000},\n\tjournal = {Bulletin of Symbolic Logic},\n\tkeywords = {Logic, Geometry, Constructive mathematics},\n\tmonth = {March},\n\tnumber = {1},\n\tpages = {1-104},\n\ttitle = {Constructive geometry and the parallel postulate},\n\turl_pdf = {ConstructiveGeometryAndTheParallelPostulate.pdf},\n\tvolume = {22},\n\tyear = {2016}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 2015\n \n \n (3)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n \n Herbrand's theorem and non-Euclidean geometry.\n \n \n \n \n\n\n \n Beeson, M.; Boutry, P.; and Narboux, J.\n\n\n \n\n\n\n
Bulletin of Symbolic Logic, 21(1): 111-122. June 2015.\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@article{beeson2015c-narboux-boutry,\n\tauthor = {Michael Beeson and Pierre Boutry and Julien Narboux},\n\tdate-added = {2014-11-15 01:23:10 +0000},\n\tdate-modified = {2015-06-25 19:08:05 +0000},\n\tjournal = {Bulletin of Symbolic Logic},\n\tkeywords = {Logic, Geometry},\n\tmonth = {June},\n\tnumber = {1},\n\tpages = {111-122},\n\ttitle = {{H}erbrand's theorem and non-{E}uclidean geometry},\n\turl_pdf = {HerbrandEuclid.pdf},\n\tvolume = {21},\n\tyear = {2015}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n A constructive version of Tarski's geometry.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n
Annals of Pure and Applied Logic, 166(11): 1199-1273. 2015.\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n \n doi\n \n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@article{beeson2015b,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-11-15 01:21:33 +0000},\n\tdate-modified = {2015-10-08 17:57:18 +0000},\n\tdoi = {10.1016/j.apal.2015.07.006},\n\tjournal = {Annals of Pure and Applied Logic},\n\tkeywords = {Constructive mathematics, Geometry, Logic},\n\tnumber = {11},\n\tpages = {1199-1273},\n\ttitle = {A constructive version of {T}arski's geometry},\n\turl_pdf = {ConstructiveTarski.pdf},\n\tvolume = {166},\n\tyear = {2015},\n\tbdsk-url-1 = {http://dx.doi.org/10.1016/j.apal.2015.07.006}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n A real analytic Jordan curve cannot bound infinitely many relative minima of area.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n . 2015.\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n\n\n\n
\n
@article{beeson2015,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-11-15 01:14:46 +0000},\n\tdate-modified = {2019-10-15 11:55:06 -0700},\n\thowpublished = {ArXiv},\n\tkeywords = {Minimal surfaces},\n\ttitle = {A real analytic {J}ordan curve cannot bound infinitely many relative minima of area},\n\turl_pdf = {part3.pdf},\n\tyear = {2015}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 2014\n \n \n (1)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n \n OTTER proofs in Tarskian geometry.\n \n \n \n \n\n\n \n Beeson, M.; and Wos, L.\n\n\n \n\n\n\n In Demri, S.; Kapur, D.; and Weidenbach, C., editor(s),
7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, Vienna, Austria, July 19-22, 2014, Proceedings, volume 8562, of
Lecture Notes in Computer Science, pages 495-510, 2014. Springer\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{beeson2014-wos,\n\tauthor = {Michael Beeson and Larry Wos},\n\tbooktitle = {7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, Vienna, Austria, July 19-22, 2014, Proceedings},\n\tdate-added = {2014-11-13 22:38:34 +0000},\n\tdate-modified = {2018-01-29 08:27:18 +0000},\n\teditor = {St{\\'e}phane Demri and Deepak Kapur and Christoph Weidenbach},\n\tkeywords = {Geometry, Automated deduction},\n\tpages = {495-510},\n\tpublisher = {Springer},\n\tseries = {Lecture Notes in Computer Science},\n\ttitle = {OTTER proofs in {T}arskian geometry},\n\turl_pdf = {TarskiFormalization.pdf},\n\tvolume = {8562},\n\tyear = {2014}}\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 2013\n \n \n (1)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n \n Proof and Computation in Geometry.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n In Ida, T.; and Fleuriot, J., editor(s),
Automated Deduction in Geometry (ADG 2012), volume 7993, of
Springer Lecture Notes in Artificial Intelligence, pages 1-30, Berlin Heidelberg, 2013. Springer-Verlag\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{beeson2013,\n\taddress = {Berlin Heidelberg},\n\tauthor = {Michael Beeson},\n\tbooktitle = {Automated Deduction in Geometry (ADG 2012)},\n\tdate-added = {2014-11-13 22:54:27 +0000},\n\tdate-modified = {2014-11-14 18:30:43 +0000},\n\teditor = {Tetsuo Ida and Jacques Fleuriot},\n\tkeywords = {Geometry, Constructive mathematics},\n\tpages = {1-30},\n\tpublisher = {Springer-Verlag},\n\tseries = {Springer Lecture Notes in Artificial Intelligence},\n\ttitle = {Proof and Computation in Geometry},\n\turl_pdf = {Edinburgh.pdf},\n\tvolume = {7993},\n\tyear = {2013}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 2012\n \n \n (1)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n \n Logic of ruler and compass constructions.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n In Cooper, S. B.; Dawar, A.; and Loewe, B., editor(s),
Computability in Europe 2012, volume 7318, of
Theoretical Computer Science and General Issues, pages 46-55, Berlin Heidelberg, 2012. Springer-Verlag\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{beeson2012,\n\taddress = {Berlin Heidelberg},\n\tauthor = {Michael Beeson},\n\tbooktitle = {Computability in Europe 2012},\n\tdate-added = {2014-11-13 22:57:33 +0000},\n\tdate-modified = {2014-11-14 18:30:35 +0000},\n\teditor = {S. Barry Cooper and Anuj Dawar and Benedict Loewe},\n\tkeywords = {Geometry, Constructive mathematics},\n\tpages = {46-55},\n\tpublisher = {Springer-Verlag},\n\tseries = {Theoretical Computer Science and General Issues},\n\ttitle = {Logic of ruler and compass constructions},\n\turl_pdf = {Cambridge.pdf},\n\tvolume = {7318},\n\tyear = {2012}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 2011\n \n \n (1)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n \n Inconsistencies in the Process Specification Language (PSL).\n \n \n \n \n\n\n \n Beeson, M.; Halcomb, J.; and Mayer, W.\n\n\n \n\n\n\n In Höfner, P.; McIver, A.; and Struth, G., editor(s),
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, pages 9-19. CEUR, 2011.\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@incollection{beeson2011,\n\tauthor = {Michael Beeson and Jay Halcomb and Wolfgang Mayer},\n\tbooktitle = {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},\n\tdate-added = {2014-11-14 22:23:30 +0000},\n\tdate-modified = {2014-11-14 22:31:29 +0000},\n\teditor = {Peter H{\\"o}fner and Annabelle McIver and George Struth},\n\tkeywords = {Automated deduction, PSL},\n\tpages = {9-19},\n\tpublisher = {CEUR},\n\ttitle = {Inconsistencies in the Process Specification Language (PSL)},\n\turl_pdf = {PSL_Inconsistencies.pdf},\n\tyear = {2011}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 2010\n \n \n (1)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n \n Constructive Geometry.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n In Arai, T.; Brendle, J.; Chong, C.; R. Downey; Q. Feng; H. Kikyou; and H. Ono, editor(s),
Proceedings of the Tenth Asian Logic Colloquium, Kobe, Japan, 2008, pages 19-84, Singapore, 2010. World Scientific\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{beeson2010,\n\taddress = {Singapore},\n\tauthor = {Michael Beeson},\n\tbooktitle = {Proceedings of the Tenth Asian Logic Colloquium, Kobe, Japan, 2008},\n\tdate-added = {2014-11-13 23:03:00 +0000},\n\tdate-modified = {2014-11-15 01:17:11 +0000},\n\teditor = {T. Arai and J. Brendle and C.~T.~ Chong and R.~Downey and Q.~Feng and H.~Kikyou and H.~Ono},\n\tkeywords = {Geometry, Constructive mathematics},\n\tpages = {19-84},\n\tpublisher = {World Scientific},\n\ttitle = {Constructive Geometry},\n\turl_pdf = {ConstructiveGeometryFinalPreprintVersion.pdf},\n\tyear = {2010}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 2006\n \n \n (1)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n \n Mathematical Induction in Otter-lambda.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n
Journal of Automated Reasoning, 36(4): 311-344. 2006.\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n\n\n\n
\n
@article{beeson2006,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-11-13 23:07:51 +0000},\n\tdate-modified = {2014-11-14 18:30:04 +0000},\n\tjournal = {Journal of Automated Reasoning},\n\tkeywords = {Automated deduction},\n\tnumber = {4},\n\tpages = {311-344},\n\ttitle = {Mathematical Induction in {O}tter-lambda},\n\turl_pdf = {induction.pdf},\n\tvolume = {36},\n\tyear = {2006}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 2005\n \n \n (4)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n \n Implicit and explicit typing in lambda logic.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n In Benzmueller, C.; Harrison, J.; and Schuermann, C., editor(s),
LPAR-05 Workshop: Empirically Successful Automated Reasoning in Higher-Order Logic (ESHOL), 2005. \n
The first link leads to a slightly extended version. The second link leads to the entire workshop proceedings\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n \n
pdf2\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{beeson2005b,\n\tauthor = {Michael Beeson},\n\tbooktitle = {LPAR-05 Workshop: Empirically Successful Automated Reasoning in Higher-Order Logic (ESHOL)},\n\tdate-added = {2014-11-17 17:39:30 +0000},\n\tdate-modified = {2014-11-17 18:05:43 +0000},\n\teditor = {Christoph Benzmueller and John Harrison and Carsten Schuermann},\n\tkeywords = {Logic, Otter},\n\tnote = {The first link leads to a slightly extended version. The second link leads to the entire workshop proceedings},\n\ttitle = {Implicit and explicit typing in lambda logic},\n\turl_pdf = {ImplicitAndExplicitTyping.pdf},\n\turl_pdf2 = {http://arxiv.org/abs/cs/0601042},\n\tyear = {2005}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Double negation elimination in some propositional logics.\n \n \n \n \n\n\n \n Beeson, M.; Veroff, R.; and Wos, L.\n\n\n \n\n\n\n
Studia Logica, 80(2-3): 195-234. 2005.\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@article{beeson2005-veroff-wos,\n\tauthor = {Michael Beeson and Robert Veroff and Larry Wos},\n\tdate-added = {2014-11-13 23:12:48 +0000},\n\tdate-modified = {2014-11-14 18:16:30 +0000},\n\tjournal = {Studia Logica},\n\tkeywords = {Automated deduction, Logic},\n\tnumber = {2-3},\n\tpages = {195-234},\n\ttitle = {Double negation elimination in some propositional logics},\n\turl_pdf = {dn.pdf},\n\tvolume = {80},\n\tyear = {2005}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n The meaning of infinity in calculus and computer algebra systems.\n \n \n \n \n\n\n \n Beeson, M.; and Wiedijk, F.\n\n\n \n\n\n\n
Journal of Symbolic Computation, 39(5): 523-538. 2005.\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@article{beeson2005-wiedijk,\n\tauthor = {Michael Beeson and Freek Wiedijk},\n\tdate-added = {2014-11-13 23:11:09 +0000},\n\tdate-modified = {2014-11-14 16:58:28 +0000},\n\tjournal = {Journal of Symbolic Computation},\n\tkeywords = {Logic, Symbolic computation},\n\tnumber = {5},\n\tpages = {523-538},\n\ttitle = {The meaning of infinity in calculus and computer algebra systems},\n\turl_pdf = {LimitTheory.pdf},\n\tvolume = {39},\n\tyear = {2005}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Constructivity, computability, and the continuum.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n In
Essays on the Foundations of Mathematics and Logic, volume 2. Polimetrica, Milan, 2005.\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@incollection{beeson2005,\n\taddress = {Milan},\n\tauthor = {Michael Beeson},\n\tbooktitle = {Essays on the Foundations of Mathematics and Logic},\n\tdate-added = {2014-11-13 23:09:07 +0000},\n\tdate-modified = {2014-11-14 18:16:21 +0000},\n\tkeywords = {Logic, Constructive mathematics},\n\tpublisher = {Polimetrica},\n\ttitle = {Constructivity, computability, and the continuum},\n\turl_pdf = {ccc.pdf},\n\tvolume = {2},\n\tyear = {2005}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 2004\n \n \n (2)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n \n Otter-lambda, a theorem-prover with untyped lambda-unification.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n In Sutcliffe, G.; Schulz, S.; and Tammet, T., editor(s),
Proceedings of the ESFOR workshop at IJCAR 2004, 2004. \n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{beeson2004b,\n\tauthor = {Michael Beeson},\n\tbooktitle = {Proceedings of the ESFOR workshop at IJCAR 2004},\n\tdate-added = {2014-11-17 17:33:33 +0000},\n\tdate-modified = {2014-11-17 17:37:46 +0000},\n\teditor = {Geoff Sutcliffe and Stephan Schulz and Tanel Tammet},\n\tkeywords = {Automated deduction, Otter},\n\ttitle = {Otter-lambda, a theorem-prover with untyped lambda-unification},\n\turl_pdf = {esfor.pdf},\n\tyear = {2004}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Lambda Logic.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n In
Automated Reasoning: Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings, volume 3097, of
Lecture Notes in Artificial Intelligence, pages 460-474, 2004. \n
The second link is to the published version; the first link is to a revised and corrected version.\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n \n
pdf2\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{beeson2004,\n\tauthor = {Michael Beeson},\n\tbooktitle = {Automated Reasoning: Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings},\n\tdate-added = {2014-11-13 23:14:14 +0000},\n\tdate-modified = {2014-11-17 17:29:15 +0000},\n\tkeywords = {Automated deduction, Lambda calculus, Logic},\n\tnote = {The second link is to the published version; the first link is to a revised and corrected version.},\n\tpages = {460-474},\n\tseries = {Lecture Notes in Artificial Intelligence},\n\ttitle = {Lambda Logic},\n\turl_pdf = {LambdaLogic.pdf},\n\turl_pdf2 = {LambdaLogicOriginal.pdf},\n\tvolume = {3097},\n\tyear = {2004}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 2003\n \n \n (1)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n \n The mechanization of mathematics.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n In Teuscher, C., editor(s),
Alan Turing: Life and Legacy of a Great Thinker, pages 77-134. Springer-Verlag, Berlin Heidelberg New York, 2003.\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 2 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n\n\n\n
\n
@incollection{beeson2003,\n\taddress = {Berlin Heidelberg New York},\n\tauthor = {Michael Beeson},\n\tbooktitle = {Alan Turing: Life and Legacy of a Great Thinker},\n\tdate-added = {2014-11-13 23:16:55 +0000},\n\tdate-modified = {2014-11-14 18:15:34 +0000},\n\teditor = {Christopher Teuscher},\n\tkeywords = {Automated deduction},\n\tpages = {77-134},\n\tpublisher = {Springer-Verlag},\n\ttitle = {The mechanization of mathematics},\n\turl_pdf = {turing2.pdf},\n\tyear = {2003}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 2002\n \n \n (3)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n \n Solving for functions.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n In Nakagawa, K., editor(s),
LMCS 2002. Logic, Mathematics and Computer Science: Interactions. Symposium in Honor of Bruno Buchberger's 60th Birthday, Linz, Austria, 2002. RISC\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{beeson2002b,\n\taddress = {Linz, Austria},\n\tauthor = {Michael Beeson},\n\tbooktitle = {LMCS 2002. Logic, Mathematics and Computer Science: Interactions. Symposium in Honor of Bruno Buchberger's 60th Birthday},\n\tdate-added = {2014-11-17 16:42:13 +0000},\n\tdate-modified = {2014-11-17 18:05:05 +0000},\n\teditor = {Koji Nakagawa},\n\tkeywords = {Otter, Unification, Automated deduction},\n\tnumber = {RISC Technical Report 02-60},\n\tpublisher = {RISC},\n\ttitle = {Solving for functions},\n\turl_pdf = {http://www.michaelbeeson.com/research/papers/SolvingForFunctions.pdf},\n\tyear = {2002}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n MathXpert : un logiciel pour aider les élèves à apprendre les mathématiques par l'action.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n
Sciences et Techniques Educatives, 9(1-2). 2002.\n
The link is to the English original; I do not have a copy of the French published version.\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@article{beeson2002a,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-11-14 19:22:39 +0000},\n\tdate-modified = {2014-11-17 18:09:15 +0000},\n\tjournal = {Sciences et Techniques Educatives},\n\tkeywords = {MathXpert, Education},\n\tnote = {The link is to the English original; I do not have a copy of the French published version.},\n\tnumber = {1-2},\n\ttitle = {Math{X}pert : un logiciel pour aider les {\\'e}l{\\`e}ves {\\`a} apprendre les math{\\'e}matiques par l'action},\n\turl_pdf = {English-ste.pdf},\n\tvolume = {9},\n\tyear = {2002}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n The meaning of infinity in calculus and computer algebra systems.\n \n \n \n\n\n \n Beeson, M.; and Wiedijk, F.\n\n\n \n\n\n\n In Calmet, J.; Benhamou, B.; Caprotti, O.; Henocque, L.; and Sorge, V., editor(s),
Artificial Intelligence, Automated Reasoning, and Symbolic Computation: Joint International Conferences, AISC 2002 and Calculemus 2002, Marseille, France, July 2002, Proceedings, pages 246-258, 2002. \n
\n\n
\n\n
\n\n
\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{beeson2002-wiedijk,\n\tauthor = {Michael Beeson and Freek Wiedijk},\n\tbooktitle = {Artificial Intelligence, Automated Reasoning, and Symbolic Computation: Joint International Conferences, AISC 2002 and Calculemus 2002, Marseille, France, July 2002, Proceedings},\n\tdate-added = {2014-11-13 23:20:17 +0000},\n\tdate-modified = {2014-11-14 18:15:19 +0000},\n\teditor = {Jacques Calmet and Belaid Benhamou and Olga Caprotti and Laurent Henocque and Volker Sorge},\n\tkeywords = {Logic, Symbolic computation},\n\tpages = {246-258},\n\ttitle = {The meaning of infinity in calculus and computer algebra systems},\n\tyear = {2002}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 2001\n \n \n (2)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n \n A second-order theorem prover applied to circumscription.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n In Gore, R.; Leitsch, A.; and Nipkow, T., editor(s),
Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 2001, Proceedings, volume 2083, pages 318-324, 2001. Springer-Verlag\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n\n\n\n
\n
@inproceedings{beeson2001b,\n\tauthor = {Michael Beeson},\n\tbooktitle = {Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 2001, Proceedings},\n\tdate-added = {2014-11-13 23:38:15 +0000},\n\tdate-modified = {2014-11-14 19:30:37 +0000},\n\teditor = {Rajeev Gore and Alexander Leitsch and Tobias Nipkow},\n\tkeywords = {Automated deduction},\n\tpages = {318-324},\n\tpublisher = {Springer-Verlag},\n\ttitle = {A second-order theorem prover applied to circumscription},\n\turl_pdf = {circumscription.pdf},\n\tvolume = {2083},\n\tyear = {2001}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Automatic derivation of the irrationality of e.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n
Journal of Symbolic Computation, 32(4): 333-349. 2001.\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n\n\n\n
\n
@article{beeson2001,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-11-13 23:28:10 +0000},\n\tdate-modified = {2014-11-14 19:31:28 +0000},\n\tjournal = {Journal of Symbolic Computation},\n\tkeywords = {Automated deduction},\n\tnumber = {4},\n\tpages = {333-349},\n\ttitle = {Automatic derivation of the irrationality of e},\n\turl_pdf = {JSCVersion.pdf},\n\tvolume = {32},\n\tyear = {2001}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 1998\n \n \n (4)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n \n Design Principles of Mathpert: Software to support education in algebra and calculus.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n In Kajler, N., editor(s),
Computer-Human Interaction in Symbolic Computation, pages 89-115. Springer-Verlag, Berlin Heidelberg New York, 1998.\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@incollection{beeson1998a,\n\taddress = {Berlin Heidelberg New York},\n\tauthor = {Michael Beeson},\n\tbooktitle = {Computer-Human Interaction in Symbolic Computation},\n\tdate-added = {2014-11-13 23:48:07 +0000},\n\tdate-modified = {2018-01-29 08:35:21 +0000},\n\teditor = {Norman Kajler},\n\tkeywords = {MathXpert, Education},\n\tpages = {89-115},\n\tpublisher = {Springer-Verlag},\n\ttitle = {Design Principles of {M}athpert: Software to support education in algebra and calculus},\n\turl_pdf = {hisc.pdf},\n\tyear = {1998}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Automatic generation of epsilon-delta proofs of continuity.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n In Calmet, J.; and Plaza, J., editor(s),
Artificial Intelligence and Symbolic Computation, volume 1476, of
Lecture Notes in Artificial Intelligence, pages 67-83, Berlin Heidelberg New York, 1998. Springer-Verlag\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n\n\n\n
\n
@inproceedings{beeson1998d,\n\taddress = {Berlin Heidelberg New York},\n\tauthor = {Michael Beeson},\n\tbooktitle = {Artificial Intelligence and Symbolic Computation},\n\tdate-added = {2014-11-13 23:35:21 +0000},\n\tdate-modified = {2014-11-14 19:32:10 +0000},\n\teditor = {Jacques Calmet and Jan Plaza},\n\tkeywords = {Automated deduction},\n\tpages = {67-83},\n\tpublisher = {Springer-Verlag},\n\tseries = {Lecture Notes in Artificial Intelligence},\n\ttitle = {Automatic generation of epsilon-delta proofs of continuity},\n\turl_pdf = {aisc.pdf},\n\tvolume = {1476},\n\tyear = {1998}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Unification in lambda calculus with if-then-else.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n In Kirchner, C.; and Kirchner, H., editor(s),
15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings, pages 96-111, 1998. \n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{beeson1998c,\n\tauthor = {Michael Beeson},\n\tbooktitle = {15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings},\n\tdate-added = {2014-11-13 23:31:21 +0000},\n\tdate-modified = {2014-11-14 20:02:58 +0000},\n\teditor = {Claude Kirchner and Helene Kirchner},\n\tkeywords = {Unification, Automated deduction, Lambda calculus},\n\tpages = {96-111},\n\ttitle = {Unification in lambda calculus with if-then-else},\n\turl_pdf = {Unify.pdf},\n\tyear = {1998}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Reality and Truth in Mathematics.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n
Philosophia Mathematica, 6: 131-168. 1998.\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 1 download\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@article{beeson1998b,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-11-13 23:30:24 +0000},\n\tdate-modified = {2014-11-14 20:03:35 +0000},\n\tjournal = {Philosophia Mathematica},\n\tkeywords = {Logic, Constructive mathematics, Philosophy},\n\tpages = {131-168},\n\ttitle = {Reality and Truth in Mathematics},\n\turl_pdf = {reality.pdf},\n\tvolume = {6},\n\tyear = {1998}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 1997\n \n \n (3)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n \n MathXpert Calculus Assistant.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n 1997.\n
The current version of this software is sold by Help With Math.\n\n
\n\n
\n\n
\n\n \n \n
helpwithmath\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@misc{beeson1997c,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-11-14 22:41:12 +0000},\n\tdate-modified = {2019-02-28 15:18:01 -0800},\n\tkeywords = {Math{X}pert, Education, Software},\n\tnote = {The current version of this software is sold by Help With Math.},\n\tpublisher = {MathXpert Systems},\n\ttitle = {MathXpert Calculus Assistant},\n\turl_helpwithmath = {http://www.helpwithmath.com},\n\tyear = {1997}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n MathXpert Precalculus Assistant.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n 1997.\n
The current version of this software is sold by Help With Math.\n\n
\n\n
\n\n
\n\n \n \n
helpwithmath\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@misc{beeson1997b,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-11-14 22:39:49 +0000},\n\tdate-modified = {2019-02-28 15:17:51 -0800},\n\tkeywords = {MathXpert, Education, Software},\n\tnote = {The current version of this software is sold by Help With Math.},\n\tpublisher = {MathXpert Systems},\n\ttitle = {Math{X}pert Precalculus Assistant},\n\turl_helpwithmath = {http://www.helpwithmath.com},\n\tyear = {1997}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n MathXpert Algebra Assistant.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n 1997.\n
The current version of this software is sold by Help With Math.\n\n
\n\n
\n\n
\n\n \n \n
helpwithmath\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@misc{beeson1997a,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-11-14 22:36:22 +0000},\n\tdate-modified = {2019-02-28 15:17:40 -0800},\n\tkeywords = {MathXpert, Education, Software},\n\tnote = {The current version of this software is sold by Help With Math.},\n\tpublisher = {MathXpert Systems},\n\ttitle = {Math{X}pert Algebra Assistant},\n\turl_helpwithmath = {http://www.helpwithmath.com},\n\tyear = {1997}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 1995\n \n \n (1)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n \n Using nonstandard analysis to verify the correctness of computations.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n
International Journal of Foundations of Computer Science, 6(3): 299-338. 1995.\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@article{beeson1995,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-11-13 23:45:44 +0000},\n\tdate-modified = {2014-11-14 20:05:39 +0000},\n\tjournal = {International Journal of Foundations of Computer Science},\n\tkeywords = {Logic, MathXpert, Nonstandard analysis},\n\tnumber = {3},\n\tpages = {299-338},\n\ttitle = {Using nonstandard analysis to verify the correctness of computations},\n\turl_pdf = {nsappt.pdf},\n\tvolume = {6},\n\tyear = {1995}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 1992\n \n \n (3)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n \n Triangles with vertices on lattice points.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n
American Mathematical Monthly, 99(3): 243-252. 1992.\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n\n\n\n
\n
@article{beeson1992a,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-11-13 23:54:43 +0000},\n\tdate-modified = {2014-11-14 20:07:17 +0000},\n\tjournal = {American Mathematical Monthly},\n\tkeywords = {Geometry},\n\tnumber = {3},\n\tpages = {243-252},\n\ttitle = {Triangles with vertices on lattice points},\n\turl_pdf = {triangle.pdf},\n\tvolume = {99},\n\tyear = {1992}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n Mathpert: Computer support for learning algebra, trigonometry, and calculus.\n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n In Voronkov, A., editor(s),
Logic Programming and Automated Reasoning, volume 624, of
Lecture Notes in Artificial Intelligence, pages 454-457, 1992. \n
\n\n
\n\n
\n\n
\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{beeson1992b,\n\tauthor = {Michael Beeson},\n\tbooktitle = {Logic Programming and Automated Reasoning},\n\tdate-added = {2014-11-13 23:52:44 +0000},\n\tdate-modified = {2014-11-14 21:59:02 +0000},\n\teditor = {A.~ Voronkov},\n\tkeywords = {MathXpert, Symbolic computation, Education},\n\tpages = {454-457},\n\tseries = {Lecture Notes in Artificial Intelligence},\n\ttitle = {{M}athpert: Computer support for learning algebra, trigonometry, and calculus},\n\tvolume = {624},\n\tyear = {1992}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n \n Constructivism in the Nineties.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n In Czermak, J., editor(s),
Proceedings of the International Wittgenstein Symposium on Philosophy of Mathematics, Aug. 16-22, 1992, Vienna, 1992. Wittgenstein Society\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n \n \n 3 downloads\n \n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{beeson1992c,\n\taddress = {Vienna},\n\tauthor = {Michael Beeson},\n\tbooktitle = {Proceedings of the International Wittgenstein Symposium on Philosophy of Mathematics, Aug. 16-22, 1992},\n\tdate-added = {2014-11-13 23:50:51 +0000},\n\tdate-modified = {2014-11-14 20:06:33 +0000},\n\teditor = {J. Czermak},\n\tkeywords = {Logic, Constructive mathematics},\n\tpublisher = {Wittgenstein Society},\n\ttitle = {Constructivism in the Nineties},\n\turl_pdf = {const92.pdf},\n\tyear = {1992}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 1991\n \n \n (1)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n \n Some applications of Gentzen's proof theory to automated deduction.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n In Schroeder-Heister, P., editor(s),
Extensions of Logic Programming, volume 475, of Lecture Notes in Computer Science, pages 101-156. Springer-Verlag, 1991.\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@incollection{beeson1991,\n\tauthor = {Michael Beeson},\n\tbooktitle = {Extensions of Logic Programming},\n\tdate-added = {2014-11-14 21:57:08 +0000},\n\tdate-modified = {2019-10-15 11:47:36 -0700},\n\teditor = {P. Schroeder-Heister},\n\tkeywords = {Proof theory, Automated deduction},\n\tpages = {101-156},\n\tpublisher = {Springer-Verlag},\n\tseries = {Lecture Notes in Computer Science},\n\ttitle = {Some applications of {G}entzen's proof theory to automated deduction},\n\turl_pdf = {Gentzen.pdf},\n\tvolume = {475},\n\tyear = {1991}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 1990\n \n \n (1)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n A computerized environment for learning algebra, trigonometry, and calculus.\n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n
Journal of Artificial Intelligence and Education, 1: 65-76. 1990.\n
\n\n
\n\n
\n\n
\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@article{beeson1990,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-11-14 21:55:49 +0000},\n\tdate-modified = {2014-11-14 21:56:52 +0000},\n\tjournal = {Journal of Artificial Intelligence and Education},\n\tkeywords = {MathXpert, Education},\n\tpages = {65-76},\n\ttitle = {A computerized environment for learning algebra, trigonometry, and calculus},\n\tvolume = {1},\n\tyear = {1990}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 1989\n \n \n (3)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n Logic and computation in Mathpert: An expert system for learning mathematics.\n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n In
Computers and Mathematics '89, pages 202-214. Springer-Verlag, Berlin Heidelberg New York, 1989.\n
\n\n
\n\n
\n\n
\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@incollection{beeson1989c,\n\taddress = {Berlin Heidelberg New York},\n\tauthor = {Michael Beeson},\n\tbooktitle = {Computers and Mathematics '89},\n\tdate-added = {2014-11-14 21:54:16 +0000},\n\tdate-modified = {2014-11-14 21:55:33 +0000},\n\tkeywords = {MathXpert, Logic, Computation},\n\tpages = {202-214},\n\tpublisher = {Springer-Verlag},\n\ttitle = {Logic and computation in {M}athpert: An expert system for learning mathematics},\n\tyear = {1989}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n The user model in Mathpert, an expert system for learning mathematics.\n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n In Bierman; Breuker; and Sandberg, editor(s),
Artificial Intelligence and Education '89, pages 9-14, Amsterdam, 1989. IOS\n
\n\n
\n\n
\n\n
\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{beeson1989b,\n\taddress = {Amsterdam},\n\tauthor = {Michael Beeson},\n\tbooktitle = {Artificial Intelligence and Education '89},\n\tdate-added = {2014-11-14 21:52:19 +0000},\n\tdate-modified = {2014-11-14 21:53:46 +0000},\n\teditor = {Bierman and Breuker and Sandberg},\n\tkeywords = {MathXpert, Education},\n\tpages = {9-14},\n\tpublisher = {IOS},\n\ttitle = {The user model in {M}athpert, an expert system for learning mathematics},\n\tyear = {1989}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n Mathpert: An expert system for learning mathematics.\n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n In
Proceedings of the Conference on Technology in Collegiate Mathematics Education, Columbus, Ohio, October, 1988, pages 9-14, 1989. Addison-Wesley\n
\n\n
\n\n
\n\n
\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{beeson1989a,\n\tauthor = {Michael Beeson},\n\tbooktitle = {Proceedings of the Conference on Technology in Collegiate Mathematics Education, Columbus, Ohio, October, 1988},\n\tdate-added = {2014-11-14 21:49:58 +0000},\n\tdate-modified = {2014-11-14 21:54:11 +0000},\n\tkeywords = {MathXpert, Education},\n\tpages = {9-14},\n\tpublisher = {Addison-Wesley},\n\ttitle = {{M}athpert: An expert system for learning mathematics},\n\tyear = {1989}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 1988\n \n \n (2)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n \n Towards a computation system based on set theory,.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n
Theoretical Computer Science, 60: 297-340. 1988.\n
\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@article{beeson1988b,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-11-14 21:47:14 +0000},\n\tdate-modified = {2014-11-14 21:48:38 +0000},\n\tjournal = {Theoretical Computer Science},\n\tkeywords = {Logic, Set theory, Symbolic computation},\n\tpages = {297-340},\n\ttitle = {Towards a computation system based on set theory,},\n\turl_pdf = {beeson1988b.pdf},\n\tvolume = {60},\n\tyear = {1988}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n Computerizing Mathematics: Logic and Computation.\n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n In Herken, R., editor(s),
The Universal Turing Machine: A Half-Century Survey. Oxford University Press, 1988.\n
Second edition, Springer-Verlag (1994)\n\n
\n\n
\n\n
\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@incollection{beeson1988a,\n\tauthor = {Michael Beeson},\n\tbooktitle = {The Universal Turing Machine: A Half-Century Survey},\n\tdate-added = {2014-11-14 21:44:47 +0000},\n\tdate-modified = {2014-11-14 21:48:56 +0000},\n\teditor = {R. Herken},\n\tkeywords = {Logic, Computation},\n\tnote = {Second edition, Springer-Verlag (1994)},\n\tpublisher = {Oxford University Press},\n\ttitle = {Computerizing Mathematics: Logic and Computation},\n\tyear = {1988}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 1987\n \n \n (1)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n Some theories conservative over intuitionistic arithmetic.\n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n In
Logic and Computation, volume 106, of Contemporary Mathematics. American Mathematical Society, Providence, R. I., 1987.\n
\n\n
\n\n
\n\n
\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@incollection{beeson1987,\n\taddress = {Providence, R.~I.},\n\tauthor = {Michael Beeson},\n\tbooktitle = {Logic and Computation},\n\tdate-added = {2014-11-14 21:43:00 +0000},\n\tdate-modified = {2014-11-14 21:44:29 +0000},\n\tkeywords = {Logic, Constructive mathematics},\n\tpublisher = {American Mathematical Society},\n\tseries = {Contemporary Mathematics},\n\ttitle = {Some theories conservative over intuitionistic arithmetic},\n\tvolume = {106},\n\tyear = {1987}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 1986\n \n \n (1)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n Proving programs and programming proofs.\n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n In Barcus, R.; Marcus; Dorn; and Weingartner, editor(s),
Logic, Methodology, and Philosophy of Science VII, proceedings of the International Congress, Salzburg, 1983, pages 51-81, 1986. \n
This paper has been translated into French and Russian.\n\n
\n\n
\n\n
\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{beeson1986,\n\tauthor = {Michael Beeson},\n\tbooktitle = {Logic, Methodology, and Philosophy of Science VII, proceedings of the International Congress, Salzburg, 1983},\n\tdate-added = {2014-11-14 21:40:22 +0000},\n\tdate-modified = {2014-11-14 21:49:25 +0000},\n\teditor = {Ruth Barcus and Marcus and Dorn and Weingartner},\n\tkeywords = {Logic, Computation},\n\tnote = {This paper has been translated into French and Russian.},\n\tpages = {51-81},\n\ttitle = {Proving programs and programming proofs},\n\tyear = {1986}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 1985\n \n \n (2)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n \n The $6π$ theorem in minimal surfaces.\n \n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n
Pacific Journal of Mathematics, 117: 17-25. 1985.\n
The second link gives comments (written 2006) that simplify the proof and answer a question raised by Nitsche.\n\n
\n\n
\n\n
\n\n \n \n
pdf\n \n \n \n
pdf2\n \n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n\n\n\n
\n
@article{beeson1985b,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-11-14 16:50:41 +0000},\n\tdate-modified = {2014-11-17 18:13:34 +0000},\n\tjournal = {Pacific Journal of Mathematics},\n\tkeywords = {Minimal surfaces},\n\tnote = {The second link gives comments (written 2006) that simplify the proof and answer a question raised by Nitsche.},\n\tpages = {17-25},\n\ttitle = {The $6\\pi$ theorem in minimal surfaces},\n\turl_pdf = {sixpi.pdf},\n\turl_pdf2 = {sixpiReview.pdf},\n\tvolume = {117},\n\tyear = {1985}}\n\n\n
\n\n\n\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 1984\n \n \n (2)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n Church's thesis, continuity, and set theory.\n \n \n \n\n\n \n Beeson, M.; and Scedrov, A.\n\n\n \n\n\n\n
Journal of Symbolic Logic, 49: 273-308. 1984.\n
\n\n
\n\n
\n\n
\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@article{beeson1984-scedrov,\n\tauthor = {Michael Beeson and Andre Scedrov},\n\tdate-added = {2014-11-14 16:53:41 +0000},\n\tdate-modified = {2014-11-14 18:11:38 +0000},\n\tjournal = {Journal of Symbolic Logic},\n\tkeywords = {Logic, Constructive mathematics},\n\tpages = {273-308},\n\ttitle = {Church's thesis, continuity, and set theory},\n\tvolume = {49},\n\tyear = {1984}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n The cusp catastrophe of Thom in the bifurcation of minimal surfaces.\n \n \n \n\n\n \n Beeson, M.; and Tromba, A. J.\n\n\n \n\n\n\n
Manuscripta Mathematica, 46: 273-308. 1984.\n
\n\n
\n\n
\n\n
\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n\n\n\n
\n
@article{beeson1984-tromba,\n\tauthor = {Michael Beeson and Anthony J. Tromba},\n\tdate-added = {2014-11-14 16:52:15 +0000},\n\tdate-modified = {2018-02-13 00:48:28 +0000},\n\tjournal = {Manuscripta Mathematica},\n\tkeywords = {Minimal surfaces},\n\tpages = {273-308},\n\ttitle = {The cusp catastrophe of {T}hom in the bifurcation of minimal surfaces},\n\tvolume = {46},\n\tyear = {1984}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 1982\n \n \n (3)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n Some results on finiteness in Plateau's problem, Part II.\n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n
Mathematische Zeitschrift, 181: 1-30. 1982.\n
\n\n
\n\n
\n\n
\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n\n\n\n
\n
@article{beeson1982b,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-11-14 21:38:25 +0000},\n\tdate-modified = {2014-11-14 22:10:52 +0000},\n\tjournal = {Mathematische Zeitschrift},\n\tkeywords = {Minimal surfaces},\n\tpages = {1-30},\n\ttitle = {Some results on finiteness in {P}lateau's problem, Part {II}},\n\tvolume = {181},\n\tyear = {1982}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n Problematic principles in constructive mathematics.\n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n In van Dalen, D.; D. Lascar; and J. Smiley, editor(s),
Logic Colloquium '80, pages 11-55, Amsterdam, 1982. North-Holland\n
\n\n
\n\n
\n\n
\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{beeson1982c,\n\taddress = {Amsterdam},\n\tauthor = {Michael Beeson},\n\tbooktitle = {Logic Colloquium '80},\n\tdate-added = {2014-11-14 21:03:24 +0000},\n\tdate-modified = {2014-11-14 22:13:45 +0000},\n\teditor = {Dirk van Dalen and D.~Lascar and J.~Smiley},\n\tkeywords = {Logic, Constructive mathematics},\n\tpages = {11-55},\n\tpublisher = {North-Holland},\n\ttitle = {Problematic principles in constructive mathematics},\n\tyear = {1982}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n Recursive models for constructive set theories.\n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n
Annals of Mathematical Logic, 23: 127-178. 1982.\n
\n\n
\n\n
\n\n
\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@article{beeson1982a,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-11-14 16:55:21 +0000},\n\tdate-modified = {2014-11-14 18:11:32 +0000},\n\tjournal = {Annals of Mathematical Logic},\n\tkeywords = {Logic, Constructive mathematics, Proof theory},\n\tpages = {127-178},\n\ttitle = {Recursive models for constructive set theories},\n\tvolume = {23},\n\tyear = {1982}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 1981\n \n \n (1)\n \n \n
\n
\n
\n\n
\n
\n \n 1980\n \n \n (3)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n Extensionality and choice in constructive mathematics.\n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n
Pacific Journal of Mathematics, 88: 1-28. 1980.\n
\n\n
\n\n
\n\n
\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@article{beeson1980c,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-11-14 21:01:14 +0000},\n\tdate-modified = {2014-11-14 21:02:51 +0000},\n\tjournal = {Pacific Journal of Mathematics},\n\tkeywords = {Logic, Constructive mathematics},\n\tpages = {1-28},\n\ttitle = {Extensionality and choice in constructive mathematics},\n\tvolume = {88},\n\tyear = {1980}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n Some results on finiteness in Plateau's problem, Part I.\n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n
Mathematische Zeitschrift, 175: 103-122. 1980.\n
\n\n
\n\n
\n\n
\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n\n\n\n
\n
@article{beeson1980b,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-11-14 17:04:19 +0000},\n\tdate-modified = {2014-11-14 22:10:41 +0000},\n\tjournal = {Mathematische Zeitschrift},\n\tkeywords = {Minimal surfaces},\n\tpages = {103-122},\n\ttitle = {Some results on finiteness in {P}lateau's problem, Part {I}},\n\tvolume = {175},\n\tyear = {1980}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n On interior branch points of minimal surfaces.\n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n
Mathematische Zeitschrift, 175: 103-123. 1980.\n
\n\n
\n\n
\n\n
\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n\n\n\n
\n
@article{beeson1980a,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-11-14 17:02:06 +0000},\n\tdate-modified = {2014-11-14 18:11:05 +0000},\n\tjournal = {Mathematische Zeitschrift},\n\tkeywords = {Minimal surfaces},\n\tpages = {103-123},\n\ttitle = {On interior branch points of minimal surfaces},\n\tvolume = {175},\n\tyear = {1980}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 1979\n \n \n (2)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n Continuity in intuitionistic set theories.\n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n In M. Boffa; van Dalen, D.; D. Lascar; and J. Smiley, editor(s),
Logic Colloquium '78, Amsterdam, 1979. North-Holland\n
\n\n
\n\n
\n\n
\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@inproceedings{beeson1979b,\n\taddress = {Amsterdam},\n\tauthor = {Michael Beeson},\n\tbooktitle = {Logic Colloquium '78},\n\tdate-added = {2014-11-14 17:14:38 +0000},\n\tdate-modified = {2014-11-14 18:10:55 +0000},\n\teditor = {M.~Boffa and Dirk van Dalen and D.~Lascar and J.~Smiley},\n\tkeywords = {Logic, Constructive mathematics},\n\tpublisher = {North-Holland},\n\ttitle = {Continuity in intuitionistic set theories},\n\tyear = {1979}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n Goodman's theorem and beyond.\n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n
Pacific Journal of Mathematics, 84: 1-16. 1979.\n
\n\n
\n\n
\n\n
\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@article{beeson1979a,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-11-14 17:13:46 +0000},\n\tdate-modified = {2014-11-14 18:10:48 +0000},\n\tjournal = {Pacific Journal of Mathematics},\n\tkeywords = {Logic, Constructive mathematics},\n\tpages = {1-16},\n\ttitle = {Goodman's theorem and beyond},\n\tvolume = {84},\n\tyear = {1979}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 1978\n \n \n (2)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n Some relations between classical and constructive mathematics.\n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n
Journal of Symbolic Logic, 43: 228-246. 1978.\n
\n\n
\n\n
\n\n
\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n\n\n\n
\n
@article{beeson1978b,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-11-17 16:37:21 +0000},\n\tdate-modified = {2014-11-17 18:04:36 +0000},\n\tjournal = {Journal of Symbolic Logic},\n\tkeywords = {Constructive mathematics, Logic},\n\tpages = {228-246},\n\ttitle = {Some relations between classical and constructive mathematics},\n\tvolume = {43},\n\tyear = {1978}}\n\n\n
\n\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n A type-free Gödel interpretation.\n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n
Journal of Symbolic Logic, 43: 213-227. 1978.\n
\n\n
\n\n
\n\n
\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n \n \n \n \n\n\n\n
\n
@article{beeson1978a,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-11-14 17:00:54 +0000},\n\tdate-modified = {2014-11-17 16:37:19 +0000},\n\tjournal = {Journal of Symbolic Logic},\n\tkeywords = {Logic, Constructive mathematics, Proof theory},\n\tpages = {213-227},\n\ttitle = {A type-free {G}{\\"o}del interpretation},\n\tvolume = {43},\n\tyear = {1978}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 1977\n \n \n (4)\n \n \n
\n
\n \n \n
\n
\n\n \n \n \n \n \n Non-continuous dependence of surfaces of least area on the boundary curve.\n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n
Pacific Journal of Mathematics,11-17. 1977.\n
\n\n
\n\n
\n\n
\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n\n\n\n
\n
@article{beeson1977c,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-11-14 17:12:47 +0000},\n\tdate-modified = {2014-11-14 18:10:08 +0000},\n\tjournal = {Pacific Journal of Mathematics},\n\tkeywords = {Minimal surfaces},\n\tpages = {11-17},\n\ttitle = {Non-continuous dependence of surfaces of least area on the boundary curve},\n\tyear = {1977}}\n\n\n
\n\n\n\n
\n\n\n
\n\n\n
\n\n\n
\n
\n\n \n \n \n \n \n The behavior of a minimal surface in a corner.\n \n \n \n\n\n \n Beeson, M.\n\n\n \n\n\n\n
Archive of Rational Mechanics and Analysis, 65: 213-227. 1977.\n
\n\n
\n\n
\n\n
\n\n \n\n \n\n \n link\n \n \n\n bibtex\n \n\n \n\n \n\n \n \n \n \n \n \n \n\n \n \n \n \n \n\n\n\n
\n
@article{beeson1977d,\n\tauthor = {Michael Beeson},\n\tdate-added = {2014-11-14 16:56:55 +0000},\n\tdate-modified = {2014-11-14 18:10:25 +0000},\n\tjournal = {Archive of Rational Mechanics and Analysis},\n\tkeywords = {Minimal surfaces},\n\tpages = {213-227},\n\ttitle = {The behavior of a minimal surface in a corner},\n\tvolume = {65},\n\tyear = {1977}}\n\n\n
\n\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 1976\n \n \n (3)\n \n \n
\n
\n \n \n
\n\n\n
\n\n\n
\n\n\n\n\n\n
\n
\n\n
\n
\n \n 1972\n \n \n (1)\n \n \n
\n
\n
\n\n\n\n\n