Otter is an
automated theorem prover
Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a ma ...
developed by
William McCune at
Argonne National Laboratory
Argonne National Laboratory is a science and engineering research national laboratory operated by UChicago Argonne LLC for the United States Department of Energy. The facility is located in Lemont, Illinois, outside of Chicago, and is the lar ...
in Illinois. Otter was the first widely distributed, high-performance theorem prover for
first-order logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quanti ...
, and it pioneered a number of important implementation techniques. ''Otter'' is an acronym for ''Organized Techniques for Theorem-proving and Effective Research''.
Description
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 In computer science, a term index is a data structure to facilitate fast lookup of terms and clauses in a logic program, deductive database, or automated theorem prover.
Overview
Many operations in automatic theorem provers require search in hu ...
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 public domain (PD) consists of all the creative work to which no exclusive intellectual property rights apply. Those rights may have expired, been forfeited, expressly waived, or may be inapplicable. Because those rights have expired, ...
. The
University of Chicago
The University of Chicago (UChicago, Chicago, U of C, or UChi) is a private university, private research university in Chicago, Illinois. Its main campus is located in Chicago's Hyde Park, Chicago, Hyde Park neighborhood. The University of Chic ...
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
*
Mace4
Notes
References
*
External links
Otter home page*
Free theorem provers
Public-domain software
{{logic-stub