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).