Otter_(theorem_prover)
Otter (theorem prover)
Automated theorem prover
Otter is an automated theorem prover developed by William McCune at Argonne National Laboratory in Illinois. Otter was the first widely distributed, high-performance theorem prover for first-order logic, and it pioneered a number of important implementation techniques. Otter is an acronym for Organized Techniques for Theorem-proving and Effective Research.
This article needs additional citations for verification. (March 2012) |