There are dozens of theorem provers available and in use in the
world^{3}. The majority of
these are based on classical predicate or propositional
logic. However, there are only a few systems, including Watson, that
have the power to perform reasoning in a higher order logic. In
addition some provers are interactive like Watson whereas others are
much more automated. It is appropriate to limit detailed consideration
to interactive higher-order logic systems in this section due to space
limitations of this paper. A complete treatment would compare the
propositional, predicate, tableau and other capabilities of Watson with
respect to systems that support those styles of reasoning.

In our laboratory we have passing experience with several theorem proving systems, but have really focused our efforts on HOL [11,3] and Watson. In this section we first provide the mathematical comparison between Watson and other systems and then provide a more detailed comparison to the HOL system.