This article needs additional citations for verification. (March 2012) |
Original author(s) | William McCune |
---|---|
Written in | C |
Type | Automated theorem proving |
Website | www |
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.