Otter (theorem prover)

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.

This article is about the automated theorem prover. For the infrastructure automation tool, see Otter (software).
Otter
Original author(s)William McCune
Written inC
TypeAutomated theorem proving
Websitewww.mcs.anl.gov/research/projects/AR/otter/ Edit this on Wikidata

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.[1] Otter also pioneered the use of efficient term indexing techniques to speed up the search for inference partners in large clause sets.[2]

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."[3]

According to Wos and Pieper, OTTER is written in approximately 28,000 lines of C programming language.[4]: 89–91 

See also

Notes
  1. McCune, William; Larry Wos (1997). "Otter: The CADE-13 Competition Incarnations". Journal of Automated Reasoning. 18 (2): 211–220. doi:10.1023/A:1005843632307.
  2. McCune, William (1992). "Experiments with Discrimination-Tree Indexing and Path Indexing for Term Retrieval". Journal of Automated Reasoning. 9 (2): 147–167. doi:10.1007/BF00245458.
  3. File name Legal in the tarball
  4. Wos, Larry; Pieper, Gail W. (1999). "3.11 OTTER and Earlier Automated Theorem-Proving Programs". A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning. World Scientific. ISBN 978-9810239107.

References
  • Kalman, John Arnold (February 2001). Automated Reasoning with OTTER. Rinton Press. ISBN 978-1589490048.


This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.