Abstract
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 sale 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.
| Original language | English |
|---|---|
| Pages (from-to) | 357-408 |
| Number of pages | 52 |
| Journal | Journal of Automated Reasoning |
| Volume | 26 |
| Issue number | 4 |
| DOIs | |
| State | Published - May 2001 |
Keywords
- Equational reasoning
- Higher-order logic
- New Foundations
- Theorem prover description
- Type theory