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**
(1985) 17-25.

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).

triangle.dvi
(46kb)

triangle.ps
(1.3mb)

triangle.pdf
(0.8mb)

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**,Springer-Verlag (1992).

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
(1995) 299-338.

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
York (1998).

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)

pdf (0.9mb)

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*,1998.

ps (153 kb, 38 pp.)

ps (2 mb, 38 pp.)

ps.gz (640 kb)

42. Unification in lambda calculus with if-then-else, in *Proceedings of
the Fifteenth Conference on Automated Deduction (CADE-15)*, pp. 96-111,
Springer-Verlag (1998).

Abstract.

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). This 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, be
sure to save the many .gif files that go with it.

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: *Proceedings of LMCS conference in Linz, Austria, October, 2002*.

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 NewYork, 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 theoretical 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.

dvi(96 kb)

pdf(170 kb)

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 (197 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, accepted for publication in the *Journal of Automated Reasoning*. This is the final version, sent to the publisher in May, 2006. Publication is planned for the last half of 2006.

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. A real-analytic Jordan curve cannot bound infinitely many relative minima of area.

dvi(232 kb, 52 pages)

pdf(341 kb, 52 pages)

This is a paper about minimal surfaces, completing the work begun in papers 15 and 19 above (twenty-five years ago). I've been checking and improving this proof now and then since 2001. I intend to submit it for publication in summer 2006.

57. 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 .