19.num/RJF.dooley
.ls 2
.na
.LP
Software Support for Mathematical Reasoning

Samuel S. Dooley

(Professor R. J. Fateman)

NSF Graduate Fellowship, UCB Microelectronics Fellowship,
(NSF) MDR-85-50596, (NSF) MDR-87-51523, (NSF) MDR-90-50008,
(NSF) CDA-87-22788, (NSF) CCR-88-12843,
(ARPA) N00039-84-C-0089, and (ARPA) N00039-88-C-0292

Computer algebra systems perform symbolic mathematical computations.
Mathematical theorem proving systems search for derivations of
mathematical statements. Each type of system is designed to assist a
different aspect of mathematical reasoning, yet neither has been
generally successful in assisting in the task of organizing and presenting
a mathematical argument. I believe it is possible to synthesize
these two approaches to mathematical reasoning in the context of an
audited mathematical reasoning environment. The goal of such an
environment is to allow the statement, manipulation, exploration,
presentation, and derivation of mathematical statements. The primary
motivational principle in the design of such an environment is that the
user should be the final arbiter in judging whether or not a given
statement is true, instead of the mathematical software system. A user
should be able to pursue alternative courses of action if not
convinced that a given result is correct, either because the result
violates some obvious (to the user) fact about the domain of discourse,
or because not enough detail (or too much detail) has been provided to
make the explanation clear.

[1]	T. A. Ager and S. Dooley,
"Naturalizing Computer Algebra for Mathematical Reasoning,"
in
MAA Notes,
ed. Z. Karian (to appear).

[2]	T. A. Ager, R. Ravaglia, and S. Dooley,
"Representation of Inference in Computer Algebra Systems
with Applications to Intelligent Tutoring," in
Computers and Mathematics,
ed. E. Kaltofen and S. M. Watt, Springer-Verlag, New York, June
1989, pp. 215-227.

[3]	S. Dooley, "The Use of Domain Restrictions in Computer Algebra
Systems,"
M.S. thesis, UC Berkeley, December 1988.