There are dozens of theorem provers available and in use in the world3. 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.