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).
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
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.
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.)
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.
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.
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.
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).
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.
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.
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.
A preliminary version of this paper was presented at the ESHOL workshop at LPAR-12, December, 2005. Here's the ESHOL version:
The entire workshop proceedings can be found at http://arxiv.org/abs/cs/0601042 .