29 May 2002
Biographical Sketch
I received a B.A. in mathematics from the University of Notre Dame in
1978. I attended graduate school at the University of
Wisconsin-Madison, receiving an M.A. in mathematics in 1980, an
M.S. in computer sciences in 1983, and a Ph.D. in mathematics in 1984.
From 1985 to 1997, I was a research scientist at The MITRE Corporation
where I conducted research in computer theorem proving, formal methods
of computing, and information security. After leaving MITRE, I taught
at St. Cloud State University from 1997 to 1999, and joined McMaster
University in 1999.
Research Interests
My primary research interests are now applied logic, mechanized
mathematics, and rigorous methods of software development. I am
especially interested in the logical foundations of mechanized
mathematics and the little theories method for organizing mathematical
knowledge. From 1990 to 1993, I was the principal investigator of a
MITRE-Sponsored Research project to develop the IMPS Interactive Mathematical Proof
System. The project produced a new logic and methodology for
formalizing mathematics as well as the design and implementation of
the IMPS system consisting of over 70,000 lines of Lisp code. I am
currently leading a project called MathScheme. Its
objective is to integrate and generalize computer theorem proving and
computer algebra. MathScheme has received "seed" funding from Bell
Canada and MITACS, a Canadian Network of Centres of Excellence (NCE)
devoted to the Mathematics of Information Technology and Complex
Systems.
Position Statement
Mathematical knowledge is vital to all science and engineering.
However, the body of mathematical knowledge -- which is immense and
growing bigger every day -- is largely inaccessible to scientists and
engineers. Most new mathematics has never been written down; the
highlights are presented in mathematical journals, but the details
reside only in the minds of mathematicians. Computer algebra systems
embody tremendous amounts of mathematical knowledge, but they reveal
only the answers to queries, not how the answers were computed or why
they are known to be correct. Computer theorem proving systems
contain powerful deductive reasoning mechanisms and carefully
organized libraries of mathematical knowledge, yet exceedingly few
mathematics practitioners possess the background and dedication needed
to use them. Relatively little mathematics is presented on the Web;
there is no worldwide digital library of mathematics.
Sophisticated, computer-supported organization and management is
needed to make mathematical knowledge widely accessible. Mathematical
knowledge must be stored in general forms from which specific
mathematical facts can be generated on the fly as needed. The
background context of the assumptions and definitions in force must be
fully captured and open to the user. The user must have the freedom
to ignore or examine the details of how an answer was computed or why
a statement is true. The great interconnectedness of mathematics
must be represented in a way that enables the user to freely switch
from one perspective to another. And the user needs to be able to
read and write mathematics using his or her own notation and
conventions.
Mathematics is a process of creating mathematical models, exploring
them using deduction, computation, and visualization, and connecting
them when they share structure. Mathematical knowledge is a byproduct
of the process. Managing the mathematics process is key to managing
mathematical knowledge. Scientists, engineers, and mathematicians
need knowledge about existing models, but they also need knowledge
about the new models they create. In most cases, new models are
created by modifying or extending existing models. If the process
that was used to produce and study these existing models was well
managed, knowledge about the new models can be efficiently discovered
and, in some cases, even automatically generated. Mathematical
knowledge divorced from the process that produced it is like a theorem
whose proof is forgotten.