BibBase beeson, m
generated by bibbase.org
  2022 (2)
Euclid after computer proof-checking. Beeson, M. The American Mathematical Monthly, 129(7): 623-646. 2022.
Euclid after computer proof-checking [pdf] pdf   link   bibtex   44 downloads  
On the Notion of Equal Figures in Euclid. Beeson, M. Beiträge zur Algebra und Geometrie. July 2022.
On the Notion of Equal Figures in Euclid [pdf] pdf   link   bibtex   20 downloads  
  2021 (2)
The Church numbers in NF set theory. Beeson, M. . 2021.
The Church numbers in NF set theory [pdf] pdf   link   bibtex   12 downloads  
Intuitionistic NF set theory. Beeson, M. . 2021.
Intuitionistic NF set theory [pdf] pdf   link   bibtex   26 downloads  
  2019 (4)
Triangle Tiling: the case $3α + 2β = π$. Beeson, M. . 2019. Available on ArXiv
Triangle Tiling: the case $3α + 2β = π$ [pdf] pdf   link   bibtex   12 downloads  
Tilings of an isosceles triangle. Beeson, M. . 2019. Available on ArXiv
Tilings of an isosceles triangle [pdf] pdf   link   bibtex   24 downloads  
Tiling an equilateral triangle. Beeson, M. . 2019. Available on ArXiv
Tiling an equilateral triangle [pdf] pdf   link   bibtex   18 downloads  
Proof-Checking Euclid. Beeson, M.; Narboux, J.; and Wiedijk, F. Annals of Mathematics and Artificial Intelligence, 85(2): 213-257. January 2019.
Proof-Checking Euclid [link]Paper   Proof-Checking Euclid [pdf] pdf   doi   link   bibtex   22 downloads  
  2018 (2)
No triangle can be cut into seven congruent triangles. Beeson, M. . 2018. Available on ArXiv
No triangle can be cut into seven congruent triangles [pdf] pdf   link   bibtex   13 downloads  
Brouwer and Euclid. Beeson, M. Indagationes Mathematicae, 29: 483-533. 2018.
Brouwer and Euclid [pdf] pdf   link   bibtex   17 downloads  
  2017 (1)
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   link   bibtex   3 downloads  
  2016 (2)
Mixing Computations and Proofs. Beeson, M. Journal of Formalized Reasoning, 9(1): 71-99. 2016.
Mixing Computations and Proofs [pdf] pdf   link   bibtex   5 downloads  
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   link   bibtex   8 downloads  
  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   link   bibtex   6 downloads  
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   link   bibtex   23 downloads  
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   link   bibtex   1 download  
  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   link   bibtex   1 download  
  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   link   bibtex   3 downloads  
  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   link   bibtex   5 downloads  
  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.
Inconsistencies in the Process Specification Language (PSL) [pdf] pdf   link   bibtex   2 downloads  
  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   link   bibtex   5 downloads  
  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   link   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   link   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   link   bibtex   3 downloads  
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   link   bibtex   7 downloads  
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   link   bibtex   6 downloads  
  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   link   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   link   bibtex   2 downloads  
  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   link   bibtex   3 downloads  
  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   link   bibtex   1 download  
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 link is to the English original; I do not have a copy of the French published version.
MathXpert : un logiciel pour aider les élèves à apprendre les mathématiques par l'action [pdf] pdf   link   bibtex   1 download  
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.
link   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   link   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   link   bibtex   2 downloads  
  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   link   bibtex  
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   link   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   link   bibtex  
Reality and Truth in Mathematics. Beeson, M. Philosophia Mathematica, 6: 131-168. 1998.
Reality and Truth in Mathematics [pdf] pdf   link   bibtex   6 downloads  
  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   link   bibtex  
MathXpert Precalculus Assistant. Beeson, M. 1997. The current version of this software is sold by Help With Math.
MathXpert Precalculus Assistant [link] helpwithmath   link   bibtex  
MathXpert Algebra Assistant. Beeson, M. 1997. The current version of this software is sold by Help With Math.
MathXpert Algebra Assistant [link] helpwithmath   link   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   link   bibtex   4 downloads  
  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   link   bibtex   2 downloads  
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.
link   bibtex  
Constructivism in the Nineties. Beeson, M. In Czermak, J., 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   link   bibtex   3 downloads  
  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   link   bibtex   3 downloads  
  1990 (1)
A computerized environment for learning algebra, trigonometry, and calculus. Beeson, M. Journal of Artificial Intelligence and Education, 1: 65-76. 1990.
link   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.
link   bibtex  
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
link   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
link   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   link   bibtex   3 downloads  
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)
link   bibtex  
  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.
link   bibtex  
  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.
link   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   link   bibtex  
Foundations of Constructive Mathematics: Metamathematical Studies. Beeson, M. of Ergebnisse der Mathematik und ihrer GrenzgebieteSpringer, Berlin Heidelberg New York Tokyo, 1985.
link   bibtex  
  1984 (2)
Church's thesis, continuity, and set theory. Beeson, M.; and Scedrov, A. Journal of Symbolic Logic, 49: 273-308. 1984.
link   bibtex  
The cusp catastrophe of Thom in the bifurcation of minimal surfaces. Beeson, M.; and Tromba, A. J. Manuscripta Mathematica, 46: 273-308. 1984.
link   bibtex  
  1982 (3)
Some results on finiteness in Plateau's problem, Part II. Beeson, M. Mathematische Zeitschrift, 181: 1-30. 1982.
link   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
link   bibtex  
Recursive models for constructive set theories. Beeson, M. Annals of Mathematical Logic, 23: 127-178. 1982.
link   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.
link   bibtex  
  1980 (3)
Extensionality and choice in constructive mathematics. Beeson, M. Pacific Journal of Mathematics, 88: 1-28. 1980.
link   bibtex  
Some results on finiteness in Plateau's problem, Part I. Beeson, M. Mathematische Zeitschrift, 175: 103-122. 1980.
link   bibtex  
On interior branch points of minimal surfaces. Beeson, M. Mathematische Zeitschrift, 175: 103-123. 1980.
link   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
link   bibtex  
Goodman's theorem and beyond. Beeson, M. Pacific Journal of Mathematics, 84: 1-16. 1979.
link   bibtex  
  1978 (2)
Some relations between classical and constructive mathematics. Beeson, M. Journal of Symbolic Logic, 43: 228-246. 1978.
link   bibtex  
A type-free Gödel interpretation. Beeson, M. Journal of Symbolic Logic, 43: 213-227. 1978.
link   bibtex  
  1977 (4)
Non-continuous dependence of surfaces of least area on the boundary curve. Beeson, M. Pacific Journal of Mathematics,11-17. 1977.
link   bibtex  
Principles of continuous choice and continuity of functions in formal systems for constructive mathematics. Beeson, M. Annals of Mathematical Logic,249-322. 1977.
link   bibtex  
Continuity and comprehension in intuitionistic formal systems. Beeson, M. Pacific Journal of Mathematics, 68: 29-40. 1977.
link   bibtex  
The behavior of a minimal surface in a corner. Beeson, M. Archive of Rational Mechanics and Analysis, 65: 213-227. 1977.
link   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.
link   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.
link   bibtex  
Derived rules of inference related to the continuity of effective operations. Beeson, M. Journal of Symbolic Logic, 41: 328-336. 1976.
link   bibtex  
  1972 (1)
The metamathematics of constructive theories of effective operations. Beeson, M. Ph.D. Thesis, Stanford, 1972.
link   bibtex