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 .