Contents

• Contents
• Introduction
• The Logic of Watson
  • Algebraic logic
  • Definition by cases
  • Stratified abstraction
  • The relationship between stratified $\lambda$-calculus and usual type theories
  • Strongly cantorian domains
• 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
• Experience with the prover
  • Experiences of users
  • Experience with mathematical content areas
• Related Work
  • Mathematical Comparison
  • HOL
  • Other Comments
• 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: