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.

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.

References

• McCune, William; Larry Wos (1997). "Otter: The CADE-13 Competition Incarnations". Journal of Automated Reasoning 18 (2): 211–220. doi:10.1023/A:1005843632307. 
• Kalman, John Arnold. Automated Reasoning with OTTER. ISBN 1-58949-004-5

See also

• MACE

External links

• Otter home page
• Prover9 home page

This logic-related article is a stub. You can help Wikipedia by expanding it.v · Categories: Logic stubs Free theorem provers Public domain software Wikimedia Foundation. 2010. Игры ⚽ Поможем написать реферат Politics of Scotland E equational theorem prover Look at other dictionaries: Otter (disambiguation) — Otters are aquatic or marine carnivorous mammals, members of the large and diverse family Mustelidae, which also includes weasels, polecats, badgers, and others. Otter may also refer to: Contents 1 Places 2 Vehicles 3 People 4 …   Wikipedia Automated theorem proving — (ATP) or automated deduction, currently the most well developed subfield of automated reasoning (AR), is the proving of mathematical theorems by a computer program. Decidability of the problem Depending on the underlying logic, the problem of… …   Wikipedia List of mathematical logic topics — Clicking on related changes shows a list of most recent edits of articles to which this page links. This page links to itself in order that recent changes to this page will also be included in related changes. This is a list of mathematical logic …   Wikipedia 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 …   Wikipedia Models And Counter-Examples — Mace stands for Models And Counter Examples , and is an automated theorem prover based on model generation[1] References ^ William McCune home site See also Otter (theorem prover) External links …   Wikipedia William McCune — Infobox Scientist name = William McCune image width= 200px caption = William McCune residence = USA nationality = American field = Computer Technology work institution = University of New Mexico known for = Otter, Mace, Prover9, Robbins… …   Wikipedia Antilogie — Calcul des propositions Pour les articles homonymes, voir Déduction. Le calcul des propositions ou calcul propositionnel est une théorie logique qui définit les lois formelles du raisonnement. C est la version moderne de la logique stoïcienne. C… …   Wikipédia en Français Calcul Des Propositions — Pour les articles homonymes, voir Déduction. Le calcul des propositions ou calcul propositionnel est une théorie logique qui définit les lois formelles du raisonnement. C est la version moderne de la logique stoïcienne. C est aussi la première… …   Wikipédia en Français Calcul propositionnel — Calcul des propositions Pour les articles homonymes, voir Déduction. Le calcul des propositions ou calcul propositionnel est une théorie logique qui définit les lois formelles du raisonnement. C est la version moderne de la logique stoïcienne. C… …   Wikipédia en Français Expression booléenne — Calcul des propositions Pour les articles homonymes, voir Déduction. Le calcul des propositions ou calcul propositionnel est une théorie logique qui définit les lois formelles du raisonnement. C est la version moderne de la logique stoïcienne. C… …   Wikipédia en Français 18+ © Academic, 2000-2024 Contact us: Technical Support, Advertising Dictionaries export, created on PHP, Joomla, Drupal, WordPress, MODx. Mark and share Search through all dictionaries Translate… Search Internet Share the article and excerpts Direct link … Do a right-click on the link above and select “Copy Link”