2017 (2)
Brouwer and Euclid. Beeson, M. Indagationes Mathematicae, to appear in a special issue devoted to Brouwer. 2017.
Brouwer and Euclid [pdf] pdf   bibtex
Finding Proofs in Tarskian Geometry. Beeson, M.; and Wos, L. Journal of Automated Reasoning, 58(1): 181--207. January 2017.
Finding Proofs in Tarskian Geometry [pdf] pdf   bibtex
  2016 (2)
Mixing Computations and Proofs. Beeson, M. Journal of Formalized Reasoning, 9(1): 71--99. 2016.
Mixing Computations and Proofs [pdf] pdf   bibtex
Constructive geometry and the parallel postulate. Beeson, M. Bulletin of Symbolic Logic, 22(1): 1-104. March 2016.
Constructive geometry and the parallel postulate [pdf] pdf   bibtex
  2015 (3)
Herbrand's theorem and non-Euclidean geometry. Beeson, M.; Boutry, P.; and Narboux, J. Bulletin of Symbolic Logic, 21(1): 111-122. June 2015.
Herbrand's theorem and non-Euclidean geometry [pdf] pdf   bibtex
A constructive version of Tarski's geometry. Beeson, M. Annals of Pure and Applied Logic, 166(11): 1199-1273. 2015.
A constructive version of Tarski's geometry [pdf] pdf   doi   bibtex
A real analytic Jordan curve cannot bound infinitely many relative minima of area. Beeson, M. . 2015.
A real analytic Jordan curve cannot bound infinitely many relative minima of area [pdf] pdf   bibtex
  2014 (1)
OTTER proofs in Tarskian geometry. Beeson, M.; and Wos, L. 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
OTTER proofs in Tarskian geometry [pdf] pdf   bibtex
  2013 (1)
Proof and Computation in Geometry. Beeson, M. 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
Proof and Computation in Geometry [pdf] pdf   bibtex
  2012 (1)
Logic of ruler and compass constructions. Beeson, M. 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
Logic of ruler and compass constructions [pdf] pdf   bibtex
  2011 (1)
Inconsistencies in the Process Specification Language (PSL). Beeson, M.; Halcomb, J.; and Mayer, W. 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. The link leads to the workshop table of contents; click to reach the paper.
bibtex   buy
  2010 (1)
Constructive Geometry. Beeson, M. 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
Constructive Geometry [pdf] pdf   bibtex
  2006 (1)
Mathematical Induction in Otter-lambda. Beeson, M. Journal of Automated Reasoning, 36(4): 311-344. 2006.
Mathematical Induction in Otter-lambda [pdf] pdf   bibtex
  2005 (4)
Implicit and explicit typing in lambda logic. Beeson, M. In Benzmueller, C.; Harrison, J.; and Schuermann, C., editor(s), LPAR-05 Workshop: Empirically Successful Automated Reasoning in Higher-Order Logic (ESHOL), 2005. The first link leads to a slightly extended version. The second link leads to the entire workshop proceedings
Implicit and explicit typing in lambda logic [pdf] pdf   Implicit and explicit typing in lambda logic [link] pdf2   bibtex
Double negation elimination in some propositional logics. Beeson, M.; Veroff, R.; and Wos, L. Studia Logica, 80(2-3): 195--234. 2005.
Double negation elimination in some propositional logics [pdf] pdf   bibtex
The meaning of infinity in calculus and computer algebra systems. Beeson, M.; and Wiedijk, F. Journal of Symbolic Computation, 39(5): 523--538. 2005.
The meaning of infinity in calculus and computer algebra systems [pdf] pdf   bibtex
Constructivity, computability, and the continuum. Beeson, M. In Essays on the Foundations of Mathematics and Logic, volume 2. Polimetrica, Milan, 2005.
Constructivity, computability, and the continuum [pdf] pdf   bibtex   buy
  2004 (2)
Otter-lambda, a theorem-prover with untyped lambda-unification. Beeson, M. In Sutcliffe, G.; Schulz, S.; and Tammet, T., editor(s), Proceedings of the ESFOR workshop at IJCAR 2004, 2004.
Otter-lambda, a theorem-prover with untyped lambda-unification [pdf] pdf   bibtex
Lambda Logic. Beeson, M. 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. The second link is to the published version; the first link is to a revised and corrected version.
Lambda Logic [pdf] pdf   Lambda Logic [pdf] pdf2   bibtex
  2003 (1)
The mechanization of mathematics. Beeson, M. In Teuscher, C., editor(s), Alan Turing: Life and Legacy of a Great Thinker, pages 77--134. Springer-Verlag, Berlin Heidelberg New York, 2003.
The mechanization of mathematics [pdf] pdf   bibtex   buy
  2002 (3)
Solving for functions. Beeson, M. 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
Solving for functions [pdf] pdf   bibtex
MathXpert : un logiciel pour aider les élèves à apprendre les mathématiques par l'action. Beeson, M. Sciences et Techniques Educatives, 9(1--2). 2002. The links are to an English translation.
MathXpert : un logiciel pour aider les élèves à apprendre les mathématiques par l'action [link] english html   MathXpert : un logiciel pour aider les élèves à apprendre les mathématiques par l'action [pdf] english pdf   bibtex
The meaning of infinity in calculus and computer algebra systems. Beeson, M.; and Wiedijk, F. 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.
bibtex
  2001 (2)
A second-order theorem prover applied to circumscription. Beeson, M. 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
A second-order theorem prover applied to circumscription [pdf] pdf   bibtex
Automatic derivation of the irrationality of e. Beeson, M. Journal of Symbolic Computation, 32(4): 333-349. 2001.
Automatic derivation of the irrationality of e [pdf] pdf   bibtex
  1998 (4)
Design Principles of Mathpert: Software to support education in algebra and calculus. Beeson, M. In Kajler, N., editor(s), Computer-Human Interaction in Symbolic Computation, pages 89--115. Springer-Verlag, Berlin Heidelberg New York, 1998.
Design Principles of Mathpert: Software to support education in algebra and calculus [pdf] pdf   bibtex   buy
Automatic generation of epsilon-delta proofs of continuity. Beeson, M. 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
Automatic generation of epsilon-delta proofs of continuity [pdf] pdf   bibtex
Unification in lambda calculus with if-then-else. Beeson, M. 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.
Unification in lambda calculus with if-then-else [pdf] pdf   bibtex
Reality and Truth in Mathematics. Beeson, M. Philosophia Mathematica, 6: 131--168. 1998.
Reality and Truth in Mathematics [pdf] pdf   bibtex
  1997 (3)
MathXpert Calculus Assistant. Beeson, M. 1997. The current version of this software is sold by Help With Math.
MathXpert Calculus Assistant [link] helpwithmath   bibtex
MathXpert Precalculus Assistant. Beeson, M. 1997. The current version of this software is sold by Help With Math.
MathXpert Precalculus Assistant [link] helpwithmath   bibtex
MathXpert Algebra Assistant. Beeson, M. 1997. The current version of this software is sold by Help With Math.
MathXpert Algebra Assistant [link] helpwithmath   bibtex
  1995 (1)
Using nonstandard analysis to verify the correctness of computations. Beeson, M. International Journal of Foundations of Computer Science, 6(3): 299--338. 1995.
Using nonstandard analysis to verify the correctness of computations [pdf] pdf   bibtex
  1992 (3)
Triangles with vertices on lattice points. Beeson, M. American Mathematical Monthly, 99(3): 243--252. 1992.
Triangles with vertices on lattice points [pdf] pdf   bibtex
Mathpert: Computer support for learning algebra, trigonometry, and calculus. Beeson, M. In Voronkov, A., editor(s), Logic Programming and Automated Reasoning, volume 624, of Lecture Notes in Artificial Intelligence, pages 454--457, 1992.
bibtex
Constructivism in the Nineties. Beeson, M. In J.~Czermak, editor(s), Proceedings of the International Wittgenstein Symposium on Philosophy of Mathematics, Aug. 16-22, 1992, Vienna, 1992. Wittgenstein Society
Constructivism in the Nineties [pdf] pdf   bibtex
  1991 (1)
Some applications of Gentzen's proof theory to automated deduction. Beeson, M. In Schroeder-Heister, P., editor(s), Extensions of Logic Programming, volume 475, of Lecture Notes in Computer Science, pages 101--156. Springer-Verlag, 1991.
Some applications of Gentzen's proof theory to automated deduction [pdf] pdf   bibtex   buy
  1990 (1)
A computerized environment for learning algebra, trigonometry, and calculus. Beeson, M. Journal of Artificial Intelligence and Education, 1: 65--76. 1990.
bibtex
  1989 (3)
Logic and computation in Mathpert: An expert system for learning mathematics. Beeson, M. In Computers and Mathematics '89, pages 202--214. Springer-Verlag, Berlin Heidelberg New York, 1989.
bibtex   buy
The user model in Mathpert, an expert system for learning mathematics. Beeson, M. In Bierman; Breuker; and Sandberg, editor(s), Artificial Intelligence and Education '89, pages 9--14, Amsterdam, 1989. IOS
bibtex
Mathpert: An expert system for learning mathematics. Beeson, M. In Proceedings of the Conference on Technology in Collegiate Mathematics Education, Columbus, Ohio, October, 1988, pages 9--14, 1989. Addison-Wesley
bibtex
  1988 (2)
Towards a computation system based on set theory,. Beeson, M. Theoretical Computer Science, 60: 297--340. 1988.
Towards a computation system based on set theory, [pdf] pdf   bibtex
Computerizing Mathematics: Logic and Computation. Beeson, M. In Herken, R., editor(s), The Universal Turing Machine: A Half-Century Survey. Oxford University Press, 1988. Second edition, Springer-Verlag (1994)
bibtex   buy
  1987 (1)
Some theories conservative over intuitionistic arithmetic. Beeson, M. In Logic and Computation, volume 106, of Contemporary Mathematics. American Mathematical Society, Providence, R.~I., 1987.
bibtex   buy
  1986 (1)
Proving programs and programming proofs. Beeson, M. 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. This paper has been translated into French and Russian.
bibtex
  1985 (2)
The 6π theorem in minimal surfaces. Beeson, M. Pacific Journal of Mathematics, 117: 17--25. 1985. The second link gives comments (written 2006) that simplify the proof and answer a question raised by Nitsche.
The 6π theorem in minimal surfaces [pdf] pdf   The 6π theorem in minimal surfaces [pdf] pdf2   bibtex
Foundations of Constructive Mathematics: Metamathematical Studies. Beeson, M. Volume 3 of Ergebnisse der Mathematik und ihrer GrenzgebieteSpringer, Berlin Heidelberg New York Tokyo, 1985.
bibtex   buy
  1984 (2)
Church's thesis, continuity, and set theory. Beeson, M.; and Scedrov, A. Journal of Symbolic Logic, 49: 273--308. 1984.
bibtex
The cusp catastrophe of Thom in the bifurcation of minimal surfaces. Beeson, M.; and Tromba, A. J. Manuscripta Mathematica, 46: 273--308. 1984.
bibtex
  1982 (3)
Some results on finiteness in Plateau's problem, Part II. Beeson, M. Mathematische Zeitschrift, 181: 1--30. 1982.
bibtex
Problematic principles in constructive mathematics. Beeson, M. In van Dalen, D.; D.~Lascar; and J.~Smiley, editor(s), Logic Colloquium '80, pages 11--55, Amsterdam, 1982. North-Holland
bibtex
Recursive models for constructive set theories. Beeson, M. Annals of Mathematical Logic, 23: 127--178. 1982.
bibtex
  1981 (1)
Formalizing constructive mathematics: why and how?. Beeson, M. In Richman, F., editor(s), Constructive Mathematics, Proceedings, New Mexico, 1980, volume 873, of Lecture Notes in Mathematics, pages 146--191, 1981.
bibtex
  1980 (3)
Extensionality and choice in constructive mathematics. Beeson, M. Pacific Journal of Mathematics, 88: 1--28. 1980.
bibtex
Some results on finiteness in Plateau's problem, Part I. Beeson, M. Mathematische Zeitschrift, 175: 103--122. 1980.
bibtex
On interior branch points of minimal surfaces. Beeson, M. Mathematische Zeitschrift, 175: 103--123. 1980.
bibtex
  1979 (2)
Continuity in intuitionistic set theories. Beeson, M. In M.~Boffa; van Dalen, D.; D.~Lascar; and J.~Smiley, editor(s), Logic Colloquium '78, Amsterdam, 1979. North-Holland
bibtex
Goodman's theorem and beyond. Beeson, M. Pacific Journal of Mathematics, 84: 1--16. 1979.
bibtex
  1978 (2)
Some relations between classical and constructive mathematics. Beeson, M. Journal of Symbolic Logic, 43: 228--246. 1978.
bibtex
A type-free Gödel interpretation. Beeson, M. Journal of Symbolic Logic, 43: 213--227. 1978.
bibtex
  1977 (4)
Non-continuous dependence of surfaces of least area on the boundary curve. Beeson, M. Pacific Journal of Mathematics, 11--17. 1977.
bibtex
Principles of continuous choice and continuity of functions in formal systems for constructive mathematics. Beeson, M. Annals of Mathematical Logic, 249--322. 1977.
bibtex
Continuity and comprehension in intuitionistic formal systems. Beeson, M. Pacific Journal of Mathematics, 68: 29--40. 1977.
bibtex
The behavior of a minimal surface in a corner. Beeson, M. Archive of Rational Mechanics and Analysis, 65: 213-227. 1977.
bibtex
  1976 (3)
The unprovability in intuitionistic formal systems of the continuity of effective operations on the reals. Beeson, M. Journal of Symbolic Logic, 41: 28--24. 1976.
bibtex
The non-derivability in intuitionistic formal systems of theorems on the continuity of effective operations. Beeson, M. Journal of Symbolic Logic, 40: 321--346. 1976.
bibtex
Derived rules of inference related to the continuity of effective operations. Beeson, M. Journal of Symbolic Logic, 41: 328--336. 1976.
bibtex
  1972 (1)
The metamathematics of constructive theories of effective operations. Beeson, M. Ph.D. Thesis, Stanford, 1972.
bibtex