Otter: An Automated Deduction System


This page is obsolete. Otter and Mace2 are now being maintained elsewhere.


The current version of Otter (which includes Mace2) is 3.3f, released in August 2004. It is unlikely that there will be any further substantial development or maintenance of Otter or Mace2.

Otter's successor is Prover9.


Contents

  1. Description
  2. Computational Environment
  3. Availability Version 3.3
  4. Documentation
  5. Example Inputs and Outputs
  6. Accomplishments
  7. Performance on the TPTP Problems
  8. Bugs and Fixes
  9. Mailing Lists
  10. Copyrights and License

Related Pages

External Work


Description

Our current automated deduction system Otter is designed to prove theorems stated in first-order logic with equality. Otter's inference rules are based on resolution and paramodulation, and it includes facilities for term rewriting, term orderings, Knuth-Bendix completion, weighting, and strategies for directing and restricting searches for proofs. Otter can also be used as a symbolic calculator and has an embedded equational programming system. Otter is a fourth-generation Argonne National Laboratory deduction system whose ancestors (dating from the early 1960s) include the TP series, NIUTP, AURA, and ITP.

Currently, the main application of Otter is research in abstract algebra and formal logic. Otter and its predecessors have been used to answer many open questions in the areas of finite semigroups, ternary Boolean algebra, logic calculi, combinatory logic, group theory, lattice theory, and algebraic geometry.


Computational Environment

Otter is coded in ANSI C and is portable, easy to install, and fast. It has been used mostly on Unix-like systems, but limited versions also run in Microsoft Windows.

Availability

The current version is Otter 3.3, and the distribution package includes Mace 2.2.

Download Otter 3.3 / Mace 2.2.


Documentation

The Otter distribution package contains all source code, installation instructions, users guides in PDF and PostScript formats, and a collection of test problems.

Otter 3.3 Reference Manual

Several books on Otter and its applications are available.


Example Inputs and Outputs

Here are the test problems from the distribution package.

Accomplishments

See the New Results Page (way out of date) for a summary of new results that have been obtained with Otter and other Argonne deduction programs.

Performance on the TPTP Problems

TPTP is a large problem set for testing first-order automated theorem-proving programs. Otter has been run on all of the TPTP problems, and the following results are available.

Otter 3.1 and MACE 1.4 on TPTP v2.3.0 (table created May 22, 2000).


Bugs and Fixes

See the Change-log File.

These changes have been made in the development version of Otter. We don't retain the source code for the intermediate versions (e.g., Otter-3.2d).

If you need any of these changes, we can give you a snapshot of the current version (source code), which should contain all of the updates listed in the Change-log (and then some).


Mailing Lists

The mailing lists have been discontinued.

Copyrights and License

See the Otter/MACE Legal Page.
These activities are projects of the Mathematics and Computer Science Division of Argonne National Laboratory.