The Watson prover has a shallow initial learning curve. Undergraduate students can learn to prove equational theorems in an algebraic style with the prover quite rapidly.
The more complex case expression and stratified abstraction facilities seem also to be accessible to the advanced undergraduate and graduate math and CS students who have been users of the system.
The use of the tactic language to write complex recursive tactics has been mostly confined to the designer and one student. All users have been able to make effective use of tactics provided in libraries.
Users do not seem to have trouble with the default order of operations of the prover, but we have provided full support for conventional order of operations for applications (such as those in education) where the use of conventional order of operations would be advisable.
Users do not seem to have trouble with the use of deBruijn levels in place of conventional variable binding; those who have done reasoning with quantifiers or higher-order functions seem to have adapted to this. Since de Bruijn levels are a notational variant on the usual treatment of bound variables (we believe it would be harder to adapt to deBruijn indices), we don't find this surprising. A tactic is available in the libraries which makes the notation for abstracts look more like standard notation: this tactic decorates each bracket term with a null occurrence of the variable bound in it at its head (e.g., [?1 + ?1] becomes [?1.?1 + ?1], where the defining theorem of the connective . is ?x.?y = ?y. Another tactic removes the annotations supplied by the first tactic.
The tactic language has been useful in several contexts. A tautology-checking tactic has been used extensively. Recently, we have implemented type inference algorithms as tactics in a theory of natural numbers, integers, rationals and reals in which manipulation of type labels (retractions with strongly cantorian range) was becoming burdensome. The use of tactics for application of theorems to subterms of the selected term, composition and conversion of tactics, and global rewriting (of more than one variety) is ubiquitous.
Watson theories can be saved and retrieved in two different ways. If one is only interested in the theorems in a theory, there are storeall and load commands which respectively store and retrieve the theorems of a given theory. If one is interested in the details of proofs (especially if one needs to change a theory by modifying the details of proofs) the correct approach is to develop a proof script in a text editor. Originally, proof scripts were run under ML using its use command, but this was too slow. The prover now has its own script command which reads scripts (which are also usually readable by the ML interpreter). Scripts can be nested in a way which supports the development of libraries of theories, though the modularity provided is not very sophisticated.
A refinement we have considered but not implemented (due to the ease of use of proof scripts) is the development and storage of ``proof objects'' which would represent proofs in a way which could be manipulated by prover functions rather than a text editor. There is a natural way to do this in Watson (proofs could be represented as tactics) but there is as yet little need for this.
Multiple theorems under construction in multiple theories can be stored on the desktop at the same time in a Watson session; this facilitates development work.
There is a facility, little-used so far, which can be used to prove theorems in one theory by analogy with theorems from another: if the user provides a match between primitives and axioms of a source theory and concepts and theorems of a target theory, theorems of the source theory can be exported to the target theory (with automatic translation of notions of the source theory to notions of the target theory as needed). This theorem export facility also allows the export of tactics; if a tactic is exported, all of the subtactics it needs will automatically be exported as well. We believe that this facility of the prover will become more important as mathematical libraries grow more extensive. We have used it in one place in the publicly available libraries to transfer a proof of complete induction and related principles between theories with conflicting notation.