The Watson Theorem Prover

Boise State University, visiting DPMMS

An interactive theorem prover developed by the author will be discussed. The prover is equational (the basic style of reasoning is algebraic; all theorems are equations which are used as rewrite rules). It supports an internal programming language based on a distinctive approach to rewriting, which has the effect that programs in the internal language (tactics) are regarded by the prover as theorems (equations) and stored in theories in the same way as pure theorems. The prover gives a special role to the properties of expressions defined by cases. The prover implements the stratified lambda-calculus, an untyped higher order logic equivalent in strength to the logic of HOL. Prover functions will be described and some demonstrations given. This work is supported by a grant from the US Army Research Office.

LS Home page or Talks in 1998/99