# Otter theorem prover

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