--- name: "otter" section: "1" platform: "linux" package: "otter" version: "3.3f-1.1" release: "Debian 8 (Jessie)" platforms: ["linux"] url: "https://new.carta.tech/otter" --- # otter(1) resolution-style theorem prover ## 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)](/anldp/1.md), [**formed**(1)](/formed/1.md), [**mace2**(1)](/mace2/1.md).\ Full documentation for **otter** is found in */usr/share/doc/otter/otter33.{html,ps.gz}*. ## AUTHOR **otter** ws written by William McCune \ This manual page was written by Peter Collingbourne \, for the Debian project (but may be used by others).