The designer gained his first appreciation of interactive theorem proving from reading about Nuprl ([7]) but there is no obvious genetic relationship between Watson and Nuprl.
The prover work would have been impossible without the availability of the programming language Standard ML ([23]), which itself is a byproduct of the development of the Edinburgh LCF theorem prover ([10]).
Watson is contrasted with such provers as Automath ([24]) or Nuprl ([7]) by the use of classical rather than constructive logic. Overall, Watson is probably most similar to HOL ([11,3]) in its outlook on things (classical higher-order logic) but it is still very different from HOL.
Watson is mostly devoted to manipulation of terms/expressions rather than to propositions (there is some treatment of propositions rather than terms in the built-in mechanisms for handling case expressions), and in this way is like rewrite rule systems (such as RRL ([20])). But it is once again remote from actual rewrite rule based provers; for example, the Knuth-Bendix algorithm ([21]) has no application to Watson so far (though it might be interesting to develop an interface between Watson and an implementation of Knuth-Bendix which would serve as a tactic generator).
Watson may share some ``look and feel'' with computer algebra systems (CAS) like Maple ([4]) and Mathematica ([27]); it looks more like a system for calculation than do most theorem provers. An interesting project would be to implement a baby CAS as a package of tactics in Watson; some work like this has been done with earlier versions of the system. Watson is much smaller than a CAS (much more is left for users to do) and is also more demanding than a CAS (computer algebra systems are not in general logically sound).
Watson is not really at all comparable to systems designed for fully automated proof like Otter ([22]) and the Boyer-Moore prover ([2]). Otter was the vehicle for the only other work we know of in which automated reasoning software has been applied to systems related to Quine's New Foundations ([18]). In principle, tactics written in Watson could effectively become automatic theorem provers (the existing tautology checker might fall into this category) but real work along these lines would require that the tactic language of Watson be given a much more efficient implementation.
Watson is distinctive in its use of an untyped logic (though some type inference is supported), in its approach to rewriting and the details of its tactic language, and in the application of the logical properties of expressions defined by cases (via a system of conditional rewriting).