Otter is an automated theorem prover developed at the Argonne National Laboratory in Illinois. It was the first widely distributed high-performance theorem prover for first-order logic, and pioneered a number of important implementation techniques.
Otter home page (http://www-unix.mcs.anl.gov/AR/otter/)
