**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.

- Contents
- Introduction
- The Logic of Watson
- The implementation of the logic in Watson
- The syntax of the term language of Watson
- Implementing algebraic logic in Watson
- Implementing case expression logic in Watson
- Implementing stratified abstraction in Watson
- The handling of variable binding: de Bruijn levels and the formal definition of substitution
- Abstraction and reduction by built-in tactics
- Examples of the implementation of abstraction in Watson
- The implementation of stratification in Watson: relative type and opacity
- Examples of the implementation of stratification
- Support for strongly cantorian domains
- Examples of the implementation of strongly cantorian domains
- Definitions in Watson
- Fine points of matching: limited higher order matching and commutative matching
- Special effects

- Experience with the prover
- Related Work
- Bibliography
- Command Reference
- Remark on Pauses and GUI Mode
- Environment Management Commands
- Navigation Commands
- Display Commands
- Declaration Commands:
- Environment modification commands:
- Proof commands:
- Theory handling commands:
- View management and theorem export:
- Tactic module commands (commands really are capitalized):
- Predeclared objects:
- Command abbreviations:

- About this document ...