M. Randall Holmes and J. Alves-Foss
Watson is a general purpose system for formal reasoning. It is an interactive equational higher-order theorem prover. The higher-order logic supported by the prover is distinctive in being type-free (it is a safe variant of Quine's NF). Watson allows the development of automated proof strategies which are represented and stored by the prover in the same way as theorems. The mathematical foundations of the prover and the way these are presented to a user are discussed. The paper also contains discussions of experiences with the prover and relations of the prover to other systems.
-calculus and usual type
theories