Otter is based on
resolution and paramodulation, constrained by term orderings similar to those in the
superposition calculus. The prover also supports positive and negative
hyperresolution and a
set-of-support strategy. Proof search is based on saturation using a version of the given-clause algorithm, and is controlled by several heuristics. There also are meta-heuristics determining search parameters automatically. Otter also pioneered the use of efficient
term indexing techniques to speed up the search for inference partners in large clause sets. Otter has been very stable for a number of years but is no longer actively developed. As of November 2008, the last changelog entry was dated 14 September 2004. A successor to Otter is
Prover9. The software is in the
public domain. The
University of Chicago has declined to assert its copyrights in this software, and it may be used, modified, and redistributed (with or without modifications) by the public. However, "NEITHER THE UNITED STATES GOVERNMENT NOR ANY AGENCY THEREOF [...] REPRESENTS THAT ITS USE WOULD NOT INFRINGE PRIVATELY OWNED RIGHTS." According to Wos and Pieper, OTTER is written in approximately 28,000 lines of
C programming language. == See also ==