NAME

       otter - resolution-style theorem prover

SYNOPSIS

       otter < input-file > output-file

DESCRIPTION

       This manual page documents briefly the otter command.

       otter  is  a resolution-style theorem-proving program for first-order logic with equality.
       otter includes the inference rules binary resolution, hyperresolution, UR-resolution,  and
       binary paramodulation. Some of its other abilities and features 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, Knuth-Bendix completion, and the hints strategy.

OPTIONS

       No command-line options are accepted; all options are given in the input file.

SEE ALSO

       anldp(1), formed(1), mace2(1).
       Full documentation for otter is found in /usr/share/doc/otter/otter33.{html,ps.gz}.

AUTHOR

       otter ws written by William McCune <otter@mcs.anl.gov>

       This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>, for  the  Debian
       project (but may be used by others).

                                        November  5, 2006                                OTTER(1)