...Summary

The format of this summary follows that used in Future Directions for Research in Symbolic Computation, Report of a Workshop on Symbolic and Algebraic Computation, A. C. Hearn (chair), Society for Industrial and Applied Mathematics, 1990. In turn, the above report credits an earlier SIAM workshop on Future Directions in Control Theory, 1989.

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

...Mathematica.$\!\!\!$ 

These are some leading proof systems. Unfortunately, we cannot list all the important systems here.

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

...sophistication.

See the Web site http://www.mcs.anl.gov/home/mccune/ar/ for information on Otter and pointers to Web pages for many other systems named in this report.

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

...competition.

Added in final draft: The 1997 competition had as the top four finishers in this category the systems Gandalf, SPASS, Otter and SETHEO, in that order. Gandalf is a theorem prover that time-slices many strategies of the type incorporated in Otter. SETHEO 1997 contains the equality procedure of E-SETHEO. That several theorem provers topped SETHEO in the 1997 competition shows that the competition can stimulate groups to work hard to bring their system to top competitive status. It also makes clear that designing deductive systems is not yet a stable art.

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

...

Now with Lucent Technologies

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

...Observers

All affiliations are as of the workshop date unless otherwise stated.

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

...Laboratories

Now with Lucent Technologies

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