Otter (theorem prover)

This article needs additional citations for verification. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed. Find sources: "Otter" theorem prover – news · newspapers · books · scholar · JSTOR (March 2012) (Learn how and when to remove this message)

Otter

Original author(s)	William McCune
Written in	C
Type	Automated theorem proving
Website	www.mcs.anl.gov/research/projects/AR/otter/

OTTER (Organized Techniques for Theorem-proving and Effective Research^[1]) 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.