1. Dissertation: The metamathematics of constructive theories of effective operations. Stanford, 1972.
2. The non-derivability in intuitionistic formal systems of theorems on the continuity of effective operations, Journal of Symbolic Logic 40 (1976) 321-346.
3. The unprovability in intuitionistic formal systems of the continuity of effective operations on the reals, Journal of Symbolic Logic 41 (1976) 18-24.
4. Derived rules of inference related to the continuity of effective operations, Journal of Symbolic Logic 41 (1976) 328-336.
5. Continuity and comprehension in intuitionistic formal systems, Pacific J. Math 68 (1977) 29-40.
6. Principles of continuous choice and continuity of functions in formal systems for constructive mathematics, Annals of Mathematical Logic 12 (1977) 249-322.
7. Non-continuous dependence of surfaces of least area on the boundary curve, Pacific J. Math 70 (1977) 11-17.
8. The behavior of a minimal surface in a corner, Arch. Rat. Mech. Anal. 65 (1977) 379-393.
9. A type-free Gödel interpretation, Journal of Symbolic Logic 43 (1978) 213-227.
10. Some relations between classical and constructive mathematics, Journal of Symbolic Logic 43 (1978) 228-246.
11. Goodman's theorem and beyond, Pacific J. Math 84 (1979) 1-16.
12. Continuity in intuitionistic set theories, in : Boffa, M., van Dalen, D., and McAloon, K. (eds.), Logic Colloquium '78, pp. 1-53. North-Holland, Amsterdam, 1979.
13. Extensionality and choice in constructive mathematics, Pacific J. Math 88 (1980) 1-28.
14. On interior branch points of minimal surfaces, Math Zeitschrift 171 (1980) 133-154.
15. Some results on finiteness in Plateau's problem, Part I, Math Zeitschrift 175 (1980) 103-123.
16. Formalizing constructive mathematics: why and how?, in Richman, F. (ed.) Constructive Mathematics, Proceedings, New Mexico, 1980}, Lecture Notes in Mathematics 873, pp. 146-191, Springer, Berlin, 1981.
17. Problematic principles in constructive mathematics, in: van Dalen, D., Lascar, D., Smiley, J. (eds.), Logic Colloquium '80, pp. 11-55, North-Holland, Amsterdam, 1982.
18. Recursive models for constructive set theories, Annals of Math. Logic 23 (1982) 127-178.
19. Some results on finiteness in Plateau's problem, Part II, Math Zeitschrift 181 (1982) 1-30.
20. (with A. J. Tromba) The cusp catastrophe of Thom in the bifurcation of minimal surfaces, Manuscripta Mathematica 46 (1984) 273-308.
21. (with A. Scedrov) Church's thesis, continuity, and set theory,Journal of Symbolic Logic 49 (1984) 630-643.
22. The 6π theorem in minimal surfaces, Pacific J. Math 117
dvi(37kb, 9 pages)
pdf(100kb, 9 pages)
In 2006 I wrote Comments on my 6π theorem (pdf, 4 pages), simplifying the proof and answering a question raised by Nitsche.
23. Foundations of Constructive Mathematics: Metamathematical Studies, Springer, Berlin/Heidelberg/New York, 1985.
24. Proving programs and programming proofs, in: Barcan, Marcus, Dorn, and Weingartner (eds.), Logic, Methodology, and Philosophy of Science VII, proceedings of the International Congress, Salzburg, 1983, pp. 51-81, North-Holland, Amsterdam (1986). This paper has been translated into French and Russian .
25. Some theories conservative over intuitionistic arithmetic, in:Sieg, W. (ed.) Logic and Computation, volume 106 in the series Contemporary Mathematics; American Mathematical Society, Providence, R.I. (1987).
26. Computerizing Mathematics: Logic and Computation, in: The Universal Turing Machine: A Half-Century Survey}, edited by Herken, R., Oxford University Press (1988). Second Edition, Springer-Verlag, Berlin/ Heidelberg/ New York (1994)
27. Towards a computation system based on set theory, Theoretical Computer Science 60 (1988) 297-340.
28. Mathpert: An expert system for learning mathematics, Proceedings of the Conference on Technology in Collegiate Mathematics Education, Columbus, Ohio, October, 1988, pp. 9-14, Addison-Wesley (1989).
29. The user model in Mathpert, an expert system for learning mathematics, in: Bierman, Breuker, and Sandberg (eds.), Artificial Intelligence and Education '89, pp. 9-14, IOS, Amsterdam (1989).
30. Logic and computation in Mathpert: An expert system for learning mathematics, in: Kaltofen and Watt (eds.), Computers and Mathematics '89, pp. 202-214, Springer-Verlag, New York/ Heidelberg/ Berlin (1989).
31. A computerized environment for learning algebra, trigonometry, and calculus, Journal of Artificial Intelligence and Education 1 (1990) 65-76.
32. Some applications of Gentzen's proof theory to automated deduction, in P. Schroeder-Heister (ed.), Extensions of Logic Programming, Lecture Notes in Computer Science 475, pp. 101-156, Springer-Verlag (1991).
33. Triangles with vertices on lattice points, American Mathematical
Monthly 99, No. 3, pp. 243-252 (1992).
34. Mathpert: Computer support for learning algebra, trigonometry, and calculus, in: A. Voronkov (ed.), Logic Programming and Automated Reasoning, Lecture Notes in Artificial Intelligence 624, 454-457. Springer-Verlag (1992). [This is a system description. You should read papers 37 or 46 instead.]
35. Constructivism in the Nineties, in: Czermak, J. (ed.), Proceedings of
the International Wittgenstein Symposium on Philosophy of Mathematics, Aug.
16-22, 1992. Wittgenstein Society, Vienna (1993).
const92.ps (1 mb, 15 pp.)
const92.ps.gz (300 kb)
const92.pdf (442 kb)
36. Using nonstandard analysis to verify the correctness of computations,
International Journal of Foundations of Computer Science, Vol. 6, No. 3
dvi (156 kb, 40 pp.)
ps (3.2 mb, 40 pp.)
ps.gz (663 kb)
37. Design Principles of Mathpert: Software to support education in
algebra and calculus, in: Kajler, N. (ed.) Computer-Human Interaction in
Symbolic Computation, pp. 89-115, Springer-Verlag, Berlin/ Heidelberg/ New
dvi (113 kb). If you take this dvi file you will also need the .eps files contained in this archive: hisc-eps.zip (31 kb).
ps (2.9 mb)
38. Mathpert Algebra Assistant (software), published by Mathpert Systems, 2211 Lawson Lane, Santa
Clara, CA. (1997).
Now available from Help With Math as MathXpert Algebra Assistant.
39. Mathpert Precalculus Assistant (software), published by Mathpert Systems, 2211 Lawson Lane, Santa
Clara, CA. (1997)
Now available from Help With Math as MathXpert Precalculus Assistant.
40. Mathpert Calculus Assistant (software), published by Mathpert Systems, 2211 Lawson Lane, Santa
Clara, CA. (1997)
Now available from Help With Math as MathXpert Calculus Assistant.
41. Reality and Truth in Mathematics, Philosophia Mathematica 6 (1998) 131-168.
dvi (153 kb, 38 pp.)
pdf (212 kb, 38 pp.)
42. Unification in lambda calculus with if-then-else, in Proceedings of
the Fifteenth Conference on Automated Deduction (CADE-15), pp. 96-111,
ps (1.1 mb)
ps.gz (0.9 mb)
43. Automatic generation of epsilon-delta proofs of continuity, in: Calment,
J., and Plaza, J. (eds.), Artificial Intelligence and Symbolic
Computation, Lecture Notes in Artificial Intelligence 1476, pp.
67-83, Springer-Verlag, Berlin/Heidelberg/New York(1998).
ps (1.4 mb, 17 pp.)
ps.gz (0.7mb, 17 pp.)
pdf (0.8mb, 17 pp.)
44. Automatic generation of a proof of the irrationality of e, Journal of
Symbolic Computation 32, No. 4 (2001), pp. 333-349.
pdf (0.9 mb, 19 pp.)
dvi (70 kb, 19 pp.)
ps (1.7 mb, 19 pp.)
45. A second-order theorem prover applied to circumscription, in: Goré, R., Leitsch, A.,
and Nipkow, T. (eds.), Automated Reasoning, First International
Joint Conference, IJCAR 2001, Siena, Italy, June 2001, Proceedings, Lecture
Notes in Artificial Intelligence 2083, Springer-Verlag (2001). The version
available for download here is longer than the published version, and contains
the complete computer-generated proof that is the subject of the paper.
dvi(46kb, 16 pages)
ps (0.8 mb, 16 pages)
pdf (0.4 mb, 16 pages)
46. MathXpert : un logiciel pour aider les élèves à apprendre les mathématiques par l'action, Sciences et Techniques Educatives 9(1-2) 2002. An English translation is available here in HTML form--just click and view: MathXpert:Learning Mathematics in the 21st Century. If you want to download it, take the pdf file instead.
47. with Freek Wiedijk: The meaning of infinity in calculus and computer algebra systems, in: Calmet, J., et. al. (eds.), Artificial Intelligence, Automated Reasoning, and Symbolic Computation: Joint International Conferences, AISC 2002 and Calculemus 2002, Marseille, France, July 2002, Proceedings, pp. 246-248, Lecture Notes in Artificial Intelligence 2385, Springer (2002).
See paper 52 below for an expanded version.
48. Solving for functions, in: Nakagawa, Koji (ed.) LMCS 2002. Logic, Mathematics and Computer Science: Interactions. Symposium in Honor of Bruno Buchberger's 60th Birthday, RISC Technical Report 02-60, Linz, Austria.
dvi (57 kb, 15 pages).
pdf(159 kb, 15 pages)
This was a preliminary report on Otter-lambda. Read Papers 50, 51, and 55 below instead.
49. The mechanization of mathematics, in Teuscher, C. (ed.) Alan Turing: Life and Legacy of a Great Thinker, pp. 77-134. Springer-Verlag, Berlin Heidelberg New York, 2003.
dvi (221 kb, 55 pages).
pdf(357 kb, 55 pages)
This is a survey article on automated deduction, written for the scientist without specialized training.
50. Lambda Logic, in Basin, David; Rusinowitch, Michael (eds.) Automated Reasoning: Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings. Lecture Notes in Artificial Intelligence 3097, pp. 460-474, Springer (2004).
This paper gives the logical basis for the prover Otter-lambda. At the time I did not realize that AC is inconsistent with lambda logic, which makes one theorem vacuously true and leaves a gap in the proof of the completeness theorem for lambda logic. These defects are repaired in the revised version; but the published version is also given here for reference. The revised version also includes the proofs omitted from the published version because of conference proceedings length limits.
Revised version (dvi, 24 pages)
Revised version (pdf, 24 pages)
Published version, dvi(62 kb, 15 pages)
Published version pdf(131 kb, 15 pages)
Two proofs were omitted from the published version of this paper to meet the 15-page length limit. Those proofs can be found here:
dvi(24 kb, 6 pages)
pdf (84 kb, 6 pages)
51. Otter-lambda, a theorem-prover with untyped lambda-unification. An earlier version of this manuscript appeared in the proceedings of the ESFOR workshop at IJCAR 2004.
This paper describes the main algorithms of Otter-lambda and gives five example proofs.
52. with Freek Wiedijk: The meaning of infinity in calculus and computer algebra systems, Journal of Symbolic Computation 39(5) (2005), pp. 523-538.
dvi (46kb, 16 pages)
ps (0.8 mb, 16 pages)
pdf (0.4 mb, 16 pages)
This is an expanded version of paper 47 in this list. We define a semantics of limit terms using filters.
53. with Robert Veroff and Larry Wos: Double negation
elimination in some propositional logics, Studia Logica 80 (2-3), pp. 195 - 234 (2005).
dvi (141 kb, 41 pages).
pdf(185 kb, 41 pages)
This is a paper about logic, published in a logic journal, not a paper about automated deduction; but many of the lemmas are proved by computer-generated proofs.
54. Constructivity, computability, and the continuum, in Sica, Giandomenico (ed.) Essays on the Foundations of Mathematics and Logic, Volume 2, Polimetrica, Milan (2005).
dvi (115 kb, 29 pages)
pdf (198 kb, 29 pages)
This is a paper about the philosophy of constructive mathematics, containing some metamathematics, some physics, some philosophy, some history, and some mathematics. It was first presented as an invited talk at the Association for Symbolic Logic's spring meeting at Stanford, March 2005.
55. Mathematical induction in Otter-lambda, Journal of Automated Reasoning 36 (4) 2006, pp. 311-344.
dvi(128 kb, 37 pages)
pdf(195 kb, 37 pages)
Copyright has been transferred to Kluwer; this posting is in accordance with the copyright transfer agreement.
56. Constructive geometry, in Arai, T. (ed.) Proceedings of the Tenth Asian Logic Colloquium, Kobe, Japan, 2008, World Scientific, Singapore, 2010. This is the final preprint version (i.e., does not use the publisher's style file but is otherwise final). Slides of a talk on this subject are available here. See also a related paper below.
pdf ( 44 pages )
dvi ( 44 pages )
57. Logic of Ruler and Compass Constructions, in S. Barry Cooper, Anuj Dawar, Benedict Loewe (editors), Computability in Europe 2012 , pp. 46-55. Springer (2012).
pdf (10 pages)
This is the final preprint version. The official published version is available at www.springerlink.com.
Complete proofs of the theorems in that paper can be found in paper 60:
58. Proof and computation in geometry, in Ida, Tetsuo and Fleuriot, Jacques (eds.), Automated Deduction in Geometry (ADG 2012), Springer Lecture Notes in Artificial Intelligence 7933, pp. 1-30, Springer, Heidelberg (2013).
pdf (30 pages)
59. Implicit and explicit typing in lambda logic, unpublished. This paper addresses the relationship between proofs in a typed logic and proofs in lambda logic such as are found by Otter-lambda.
dvi(71 kb, 15 pages)
pdf(140 kb, 15 pages)
A preliminary version of this paper was presented at the ESHOL workshop at LPAR-12, December, 2005. Here's the ESHOL version:
dvi(88 kb, 19 pages)
pdf(148 kb, 19 pages)
The entire workshop proceedings can be found at http://arxiv.org/abs/cs/0601042 .
60. (with Jay Halcomb and Wolfgang Mayer) Inconsistencies in the Process Specification Language (PSL),
61. Foundations of Constructive Geometry. This is an unfinished book manuscript, but contains many finished sections, including complete proofs of all the claims in paper 57.
pdf (250 pages)62. A real analytic Jordan curve cannot bound infinitely many relative minima of area.
A version of this paper was posted on the Math ArXiv on Nov. 30, 2006 [paper number math.DG/0612001]. Here is the pdf on the ArXiv's website (1.7 mb), as revised on January 29, 2009. That version still contained an error, which has been corrected in the version posted here; this version also has an expanded "preliminaries" section.
dvi(307 kb, 70 pages, with one illustration)
pdf(561 kb, 70 pages, with one illustration)
Slides of a talk on this subject given to the Bay Area Differential Geometry Seminar in January 2009 are available here.