The Watson Theorem Prover

摘要

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 mathe- matical 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.