.TH OTTER 1 "November  5, 2006"
.SH NAME
otter \- resolution-style theorem prover
.SH SYNOPSIS
.B otter
<
.I input-file
>
.I output-file
.SH DESCRIPTION
This manual page documents briefly the
.B otter
command.
.PP
\fBotter\fP is a resolution-style theorem-proving program for first-order logic with equality. \fBotter\fP 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.
.SH OPTIONS
No command-line options are accepted; all options are given in the input file.
.SH SEE ALSO
.BR anldp (1),
.BR formed (1),
.BR mace2 (1).
.br
Full documentation for \fBotter\fP is found in \fI/usr/share/doc/otter/otter33.{html,ps.gz}\fP.
.SH AUTHOR
\fBotter\fP ws written by William McCune <otter@mcs.anl.gov>
.PP
This manual page was written by Peter Collingbourne <pcc03@doc.ic.ac.uk>,
for the Debian project (but may be used by others).