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 maj ...
developed by
William McCune
William Walker McCune (December 17, 1953 – May 2, 2011) was an American computer scientist and logician working in the fields of automated reasoning, algebra, logic, and formal methods. He was best known for the development of the Otter, Prover ...
at
Argonne National Laboratory
Argonne National Laboratory is a science and engineering research United States Department of Energy National Labs, national laboratory operated by University of Chicago, UChicago Argonne LLC for the United States Department of Energy. The facil ...
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''.
Description
Otter is based on
resolution
Resolution(s) may refer to:
Common meanings
* Resolution (debate), the statement which is debated in policy debate
* Resolution (law), a written motion adopted by a deliberative body
* New Year's resolution, a commitment that an individual mak ...
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 Prover9 is an automated theorem prover for first-order and equational logic developed by William McCune.
Description
Prover9 is the successor of the Otter theorem prover also developed by William McCune. Prover9 is noted for producing relatively ...
.
The software is in the
public domain
The public domain (PD) consists of all the creative work
A creative work is a manifestation of creative effort including fine artwork (sculpture, paintings, drawing, sketching, performance art), dance, writing (literature), filmmaking, ...
. The
University of Chicago
The University of Chicago (UChicago, Chicago, U of C, or UChi) is a private research university in Chicago, Illinois. Its main campus is located in Chicago's Hyde Park neighborhood. The University of Chicago is consistently ranked among the b ...
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 Mace stands for "Models And Counter-Examples", and is a model finder. Most automated theorem provers try to perform a proof by refutation on the clause normal form of the proof problem, by showing that the combination of axioms and negated conjectu ...
Notes
References
*
External links
Otter home page*
Free theorem provers
Public-domain software
{{logic-stub