Next:
Introduction
Up:
The Watson Theorem Prover
Previous:
The Watson Theorem Prover
Contents
Contents
Introduction
The Logic of Watson
Algebraic logic
Definition by cases
Stratified abstraction
The relationship between stratified
-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:
Randall Holmes
2000-11-03