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
- Description
- Computational Environment
- Availability Version 3.3
- Documentation
- Example Inputs and Outputs
- Accomplishments
- Performance on the TPTP Problems
- Bugs and Fixes
- Mailing Lists
- Copyrights and License
Related Pages
External Work
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.
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.
The current version is Otter 3.3, and the distribution
package includes Mace 2.2.
Download Otter 3.3 / Mace 2.2.
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.
-
Automated Reasoning and the Discovery of Missing and Elegant Proofs,
by L. Wos and G. W. Pieper, Rinton Press (2003).
-
Automated Reasoning with Otter,
by J. A. Kalman, Rinton Press (2001).
-
A Fascinating Country in the World of Computing:
Your Guide to Automated Reasoning ,
by Larry Wos, with Gail Pieper, World Scientific (2000).
-
Automated Deduction in Equational Logic and Cubic Curves,
by W. McCune and R. Padmanabhan, Springer-Verlag LNCS #1095 (1996).
-
The Automation of Reasoning: An Experimenter's Notebook with Otter
Tutorial,
by Larry Wos, Academic Press (1996).
-
Automated Development of Fundamental Mathematical Theories,
by Art Quaife, Kluwer Acadamic Publishers (1992).
Here are the test problems from the distribution package.
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.
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).
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).
The mailing lists
- otter-announce
- otter-help
- otter-development
have been discontinued.
See the
Otter/MACE Legal Page.
These activities are projects of the
Mathematics and Computer Science Division
of
Argonne National Laboratory.