{\sc Otter} (Organized Techniques for Theorem-proving and Effective
Research) is a resolution-style theorem-proving program for
first-order logic with equality.  {\sc Otter} includes the inference
rules binary resolution, hyperresolution, UR-resolution, and binary
paramodulation.  Some of its other abilities are conversion from
first-order formulas to clauses, forward and back subsumption,
factoring, weighting, answer literals, term ordering, forward and back
demodulation, evaluable functions and predicates, and Knuth-Bendix
completion.  {\sc Otter} is coded in C, it is free, and it is portable
to many different kinds of computer.

                        =========
                        OTTER 2.2
                        =========

The theorem prover OTTER 2.2 has been released.  Improvements over
Version 2.0 include:

  +    The ratio strategy for selecting the given clause  com-
       bines selection by weight with breadth-first search.

  +    The passive list can be used to  prevent  some  of  the
       input clauses from entering the search.

  +    New built-in $ functions perform bit operations.

  +    On UNIX systems, the user can  interrupt  Otter  during
       its search and change the flag and parameter settings.

  +    Indexing can be used for back demodulation.

  +    The notion of the answer literal has been  extended  to
       terms with $IGNORE.

  +    The inference rule negative  hyperresolution  has  been
       included.

  +    The user can assign a maximum to the number of distinct
       variables in clauses.

  +    A new automatic memory-control feature has been added.

  +    Parent lists can be ordered in a new way.

  +    $ operations during hyperresolution are much more efficient.

To obtain a copy by FTP, connect to info.mcs.anl.gov, username
anonymous, any password will do.  Go to pub/Otter/Otter-2.2, and
follow the directions in README.FTP.

Two versions of the manuals are included: one is LaTeX input and the
other is already formatted by nroff.  Let me know if you wish a paper copy.

Otter is coded in C and has been run mainly on UNIX workstations.
I have ported Otter to PC's and to Macintoshes, but I am a true
novice with those machines and it has not been extensively tested on
them.  The FTP release contains executable files for PCs and Macintoshes.

A floppy containing the PC version of Otter is included with the new
edition Larry Wos's book, "Automated Reasoning: Introduction and
Applications, McGraw-Hill, 1992".  We currently do not have a
distribution system set up for Macintosh or PC diskettes.

Please inform me (otter@mcs.anl.gov) if you take a copy by FTP.

  W. McCune
  MCS-221
  Argonne National Laboratory
  Argonne, IL  60439-4844

P.S.  Experimental version 2.2xa accepts Prolog-style operator
declarations.  See pub/Otter/README on info.mcs.anl.gov.