Man Linux: Main Page and Category List

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