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.

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

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

Current version 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)

Current version 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)

Current version 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 Kirchner, Claude and Helene (eds.) *15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings*, 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: Calmet,
Jacques., and Plaza, Jan. (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, pp. 318--324, 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-258,
Lecture Notes in Artificial Intelligence
**2385**, Springer (2002).

See paper 51 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*. 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.

52. *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.

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

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

55. Constructive geometry, in Arai, T. *et. al* (eds.) *Proceedings of the Tenth Asian Logic Colloquium, Kobe, Japan, 2008, *World Scientific, Singapore, 2010, pp. 19--84. 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. New readers, please begin with paper 62 instead.

pdf ( 44 pages )

dvi ( 44 pages )

56. Logic of ruler and compass constructions, in S. Barry Cooper, Anuj Dawar, Benedict Loewe (editors),
*How the World Computes, Turing Centenary Conference and 8th Conference on Computability in Europe 2012, CIE 2012, Cambridge, UK, June 2012, Proceedings*, pp. 46-55. Springer (2012).

This is the final preprint version. The official published version is available at www.springerlink.com.

Complete proofs of the theorems in that paper (and a correction) can be found in paper 62.

57. Proof and computation in geometry, in Ida, Tetsuo and Fleuriot, Jacques (eds.), *Automated Deduction in Geometry (ADG 2012)*, Springer Lecture Notes in Artificial Intelligence 7993, pp. 1-30, Springer, Heidelberg (2013).

58. (with Larry Wos) OTTER proofs in Tarskian geometry, in:
St/'ephane Demri and Deepak Kapur and Christoph Weidenbach (editors),
* 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, Vienna, Austria, July 19-22, 2014, Proceedings*, pp. 495-515

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

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

61. (with Jay Halcomb and Wolfgang Mayer) Inconsistencies in the Process Specification Language (PSL),
in

62. Constructive geometry and the parallel postulate

63. A constructive version of Tarski's geometry

64. (with Pierre Boutry and Julien Narboux) Herbrand's theorem and non-Euclidean geometry

65. A real analytic Jordan curve cannot bound infinitely many relative minima of area.