OTTER (Organized Techniques for Theorem-proving and Effective Research
) 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
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.
Biography
He was best known for the development of the Ot ...
at
Argonne National Laboratory
Argonne National Laboratory is a Federally funded research and development centers, federally funded research and development center in Lemont, Illinois, Lemont, Illinois, United States. Founded in 1946, the laboratory is owned by the United Sta ...
in Illinois. Otter was the first widely distributed, high-performance theorem prover for
first-order logic
First-order logic, also called predicate logic, predicate calculus, or quantificational logic, is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over ...
, 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 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 proving, automated theorem prover for first-order logic, first-order and equational logic developed by William McCune.
Description
Prover9 is the successor of the Otter (theorem prover), Otter theorem prover also dev ...
.
The software is in the
public domain
The public domain (PD) consists of all the creative work to which no Exclusive exclusive intellectual property rights apply. Those rights may have expired, been forfeited, expressly Waiver, waived, or may be inapplicable. Because no one holds ...
. The
University of Chicago
The University of Chicago (UChicago, Chicago, or UChi) is a Private university, private research university in Chicago, Illinois, United States. Its main campus is in the Hyde Park, Chicago, Hyde Park neighborhood on Chicago's South Side, 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
C (''pronounced'' '' – like the letter c'') is a general-purpose programming language. It was created in the 1970s by Dennis Ritchie and remains very widely used and influential. By design, C's features cleanly reflect the capabilities of ...
.
See also
*
Mace4
Notes
References
*
External links
Otter home page* {{Cite web , url=https://publications.anl.gov/anlpubs/2003/10/48079.pdf , title=OTTER 3.3 Reference Manual , access-date=2018-11-13 , archive-url=https://web.archive.org/web/20181113075918/https://publications.anl.gov/anlpubs/2003/10/48079.pdf , archive-date=2018-11-13 , url-status=bot: unknown
Free theorem provers
Public-domain software with source code
Free software programmed in C