<urc>
<url>ftp://info.mcs.anl.gov/pub/Otter/
<title>Otter: An Automated Deduction System
<contact>William McCune / mccune@mcs.anl.gov
<abstract>
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.
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 has also been used for research in the verification of
hardware and software.
<environment>
Otter is coded in C and is portable, simple to install, and very fast. It has
been used mostly on UNIX systems, but limited versions (included in the
distribution) also run on PCs and Macintoshes.
<description><url>http://www.mcs.anl.gov/home/mccune/ar/otter/index.html</url>
<keywords>first order logic; automatic theorem proving
<category>application
</urc>