Otter theorem prover
Encyclopedia
Otter 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.
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.
According to Wos and Pieper, OTTER is written in approximately 28,000 lines of C programming language.
Automated theorem proving
Automated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...
developed by William McCune
William McCune
William McCune was an American computer scientist working in the fields of Automated reasoning, Algebra, Logic, and Formal Methods. He was best known for the development of the Otter, Prover9, and Mace4 automated reasoning systems, and the automated proof of the Robbins conjecture using the EQP...
at Argonne National Laboratory
Argonne National Laboratory
Argonne National Laboratory is the first science and engineering research national laboratory in the United States, receiving this designation on July 1, 1946. It is the largest national laboratory by size and scope in the Midwest...
in Illinois. Otter was the first widely distributed, high-performance theorem prover for first-order logic
First-order logic
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...
, and it pioneered a number of important implementation techniques. Otter is an acronym for Organized Techniques for Theorem-proving and Effective Research.
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
Prover9 is an automated theorem prover for First-order and equational logic developed by William McCune. Prover9 is the successor of the Otter theorem prover.Prover9 is intentionally paired with Mace4, which searches for finite models and counterexamples...
.
The software is in the public domain
Public domain
Works are in the public domain if the intellectual property rights have expired, if the intellectual property rights are forfeited, or if they are not covered by intellectual property rights at all...
. The University of Chicago
University of Chicago
The University of Chicago is a private research university in Chicago, Illinois, USA. It was founded by the American Baptist Education Society with a donation from oil magnate and philanthropist John D. Rockefeller and incorporated in 1890...
has declined to assert its copyrights in this software, and it may be used, modified, and redistributed (with or without modifications) by the public.
According to Wos and Pieper, OTTER is written in approximately 28,000 lines of C programming language.