Numbers in the following list are not consecutive because they are the same as in the List of All Publications
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)
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).
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 Computer Science 624,Springer-Verlag (1992).
36. Using nonstandard analysis to verify the correctness of computations, International Journal of Foundations of Computer Science, Vol. 6, No. 3 (1995) 299-338.
nsappt.ps (3.2 mb, 40 pp.)
nsappt.ps.gz (663 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 .
unify.ps (1.1 mb)
unify.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).
aisc.ps (1.4 mb, 17 pp.)
aisc.ps.gz (0.7mb, 17 pp.)
aisc.pdf (0.8mb, 17 pp.)
44. Automatic generation of a proof of the irrationality of e, in Armando, A., and Jebelean, T. (eds.):
Proceedings of the Calculumus Workshop, 1999,Electronic Notes in Theoretical Computer Science
23 3, 2000. Elsevier, 1999. This paper has also been accepted for
publication in a special issue of Journal of Symbolic Computation which should
appear in the very near future.
JSCVersion.pdf (0.9 mb, 19 pp.)
JSCVersion.dvi (70 kb, 19 pp.)
JSCVersion.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 which is the subject of the paper.
dvi (46kb, 16 pages)
ps (0.8 mb, 16 pages)
pdf (0.4 mb, 16 pages)
50. Double negation elimination in some propositional logics (with Robert Veroff and Larry Wos), unpublished.
dvi (86kb, 25 pages).
pdf(506kb, 25 pages)