Randall Holmes, M.; Alves-Foss, Jim The Watson theorem prover. (English) Zbl 1003.68151 J. Autom. Reasoning 26, No. 4, 357-408 (2001). Summary: 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. Cited in 1 Review MSC: 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) Keywords:formal reasoning Software:Nuprl; Maple; HOL; ML; OTTER; LCF; Mathematica; Watson; IMPS PDFBibTeX XMLCite \textit{M. Randall Holmes} and \textit{J. Alves-Foss}, J. Autom. Reasoning 26, No. 4, 357--408 (2001; Zbl 1003.68151) Full Text: DOI