The Watson prover has been used to develop theories of propositional and predicate logic in several styles. An equational style (as exemplified in ) is most natural, and theories implementing the propositional and predicate logic chapters of  in detail exist. We have also implemented a sequent calculus and a goal driven natural deduction prover. A tableau approach to first-order logic has natural relationships with Watson's built-in logic of case expressions, and a tableau approach to propositional logic has been used to develop a complete tautology checker as a tactic. A goal-directed natural deduction prover has been implemented as an interactive tactic using the INPUT command.
Watson's notation for propositional logic presents no difficulties. Experience leads us to believe that users can readily adapt to the somewhat nonstandard notation for quantifiers. There are few problems with the stratification functions of the prover as long as the boolean type has been declared as strongly cantorian and the propositional connectives and quantifiers made scin or scout as appropriate.
The prover has been used to develop theories of basic arithmetic and algebra needed for the projected computer science applications. Watson readily supports algebraic reasoning; its case expression machinery allows a natural way to handle exceptions to algebraic rules (such as those occasioned by the need to avoid division by zero) which are usually ignored by computer algebra systems, making the typical CAS logically unsound. We have also shown that Watson is a practical environment for carrying out proofs by induction in a development of Peano arithmetic. A theory of program semantics based on  is under construction. A student has recently completed a master's project involving the verification of published proofs of security properties of communication protocols using Watson.
For example, students working on this project have been able to develop the following theory files (this list is not exhaustive):
The designer has developed a theory of synthetic combinatory logic, with a variety of different abstraction and reduction tactics, which he hopes to use as a research tool in collaboration with a specialist in this area. The fact that the prover is good for this application area is not surprising, as the development of the control structures of the tactic language was largely driven by the now abandoned attempt to use a synthetic combinatory logic rather than a -calculus as the logic of the prover.