** Next:** Bibliography
** Up:** Related Work
** Previous:** HOL

We describe a research direction for Watson which takes us into the
area of automated proof. Watson supplies a command which will tell
the user if it is possible to convert the currently displayed term to
a desired form in a single step; we have extended this feature so that
it will search for two-step proofs (in which two theorems are applied
as rewrite rules). Beyond two steps, the explosion in size of the
search space becomes a problem. After discussions with a colleague
who works in parallel programming, we think that it may be possible to
increase the efficiency of an algorithm which searches automatically
for proofs involving a few rewriting steps by applying parallel
programming techniques, and we hope to start doing research in this
area in the not too distant future. (In addition, the search could be made
more effective by applying heuristic or AI based search strategies for
multi-step solutions. This is currently not a focus of the research group.)
Our interest is not in completely automating proofs, but in making it
so that the prover will be a more intelligent assistant to the user
in interactive proofs.
We are philosophically interested in the distinction between a ``big
theory'' and a ``little theory'' approach advocated by the developers of
IMPS ([9]). Watson's higher-order logic is strong enough to
support a ``big theory'' approach (in which everything is ultimately
founded on concepts defined in the built-in higher order logic) but we have
provided support for a ``little theory'' approach (in which users can
axiomatize their own application areas in little theories, then fit
these theories together). Our mechanism for theorem export is
motivated by the desire to support something like the IMPS approach,
but the IMPS group can do much more impressive things with their
system: for example, it is possible in Watson to search for theorems
which apply to the currently displayed term, but it is not possible to
search for theorems in other theories on the desktop which could be
exported to the current theory and applied: IMPS has a capability
analogous to this which we would like to emulate. This is a research
direction we need to work in: the modularity provided by Watson needs
improvement.

** Next:** Bibliography
** Up:** Related Work
** Previous:** HOL
*Randall Holmes*

*2000-11-03*