Other Comments

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.