... Prover¹

We gratefully acknowledge the support of Army Research Office grants DAAH04-94-0247,DAAH04-96-1-0397, and DAAH04-96-1-0397

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... ((?x+?y)+?z)=?x+?y+?z²

Recall that the default precedence of Watson is to the right, so the right side of this equation is equivalent to ?x + (?y + ?z).

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.

... world³

A comprehensive list of theorem provers can be found at http://www-formal.stanford.edu/clt/ARS/systems.html.

.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.